thufschmitt/tix-papers
1
1
Fork 0
mirror of https://github.com/thufschmitt/tix-papers.git synced 2024-08-17 08:40:28 +03:00
Code Issues Projects Releases Wiki Activity

typing: add a grammar for types

Browse Source
This commit is contained in:
regnat 2017-04-06 16:47:33 +02:00
parent 8f9f7080b0
commit 99f594dd69
2 changed files with 25 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
common/header.tex
View File

@ -4,6 +4,7 @@
\usepackage[usenames,dvipsnames,svgnames,table]{xcolor}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{bm}
\usepackage{stmaryrd}
\usepackage{mathtools}
@ -24,17 +25,20 @@
\renewcommand{\grammarlabel}[2]{\meta{#1 #2}}
\newcommand{\meta}[1]{\ensuremath{#1}} % For meta syntax
\renewcommand{\|}{\textrm{|}}
\def\e/{\meta{e}}
\def\E/{\meta{E}}
\def\a/{\meta{a}}
\def\b/{\meta{b}}
\def\c/{\meta{c}}
\def\e/{\meta{e}}
\def\E/{\meta{E}}
\def\f/{\meta{f}}
\def\o/{\meta{o}}
\def\p/{\meta{p}}
\def\q/{\meta{q}}
\def\f/{\meta{f}}
\def\x/{\meta{x}}
\def\o/{\meta{o}}
\def\s/{\meta{s}}
\def\t/{\meta{t}}
\def\u/{\meta{u}}
\def\v/{\meta{v}}
\def\x/{\meta{x}}
\newcommand{\assign}[2]{\ensuremath{\sfrac{#2}{#1}}}
\newcommand{\assignp} [2] {\assign{#1}{#2}}

16
typing/type-system.tex
View File

@ -6,6 +6,22 @@
\maketitle{}
\section{Types}
\begin{grammar}
<t> ::= \c/ \| \t/ $\bm{\rightarrow}$ \t/
\alt \t/ $\bm{\vee}$ \t/ \| \t/ $\bm{\wedge}$ \t/ \| \t/ $\bm{\backslash}$ \t/
\alt [\meta{R}]
\alt \{ \s/ = \u/; \ldots{}; \s/ = \u/; _ = \u/ \}
<u> ::= \t/ \| ?\t/
<R> ::= \t/ \| \meta{R^{\bm{+}}} \| \meta{R}?
\| \meta{R} $\bm{\vee}$ \meta{R} \| \meta{R} $\bm{\wedge}$ \meta{R}
<\τ> ::= \t/ % No polymorphism for now
\end{grammar}
\section{Typing rules}
\begin{mathpar}
\inferrule{ }{\Gamma; x:\tau \vdash x:\tau}(Var)