1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
\documentclass{article}
\usepackage{fullpage}
\input{./macros.tex}
\newcommand{\minicoq}{\textsf{minicoq}}
\newcommand{\nonterm}[1]{\textit{#1}}
\newcommand{\terminal}[1]{\textsf{#1}}
\newcommand{\listzero}{\textit{LIST$_0$}}
\newcommand{\listun}{\textit{LIST$_1$}}
\newcommand{\sep}{\textit{SEP}}
\title{Minicoq: a type-checker for the pure \\
Calculus of Inductive Constructions}
\begin{document}
\maketitle
\section{Introduction}
\minicoq\ is a minimal toplevel for the \Coq\ kernel.
\section{Grammar of terms}
The grammar of \minicoq's terms is given in Figure~\ref{fig:terms}.
\begin{figure}[htbp]
\hrulefill
\begin{center}
\begin{tabular}{lrl}
term & ::= & identifier \\
& $|$ & \terminal{Rel} integer \\
& $|$ & \terminal{Set} \\
& $|$ & \terminal{Prop} \\
& $|$ & \terminal{Type} \\
& $|$ & \terminal{Const} identifier \\
& $|$ & \terminal{Ind} identifier integer \\
& $|$ & \terminal{Construct} identifier integer integer \\
& $|$ & \terminal{[} name \terminal{:} term
\terminal{]} term \\
& $|$ & \terminal{(} name \terminal{:} term
\terminal{)} term \\
& $|$ & term \verb!->! term \\
& $|$ & \terminal{(} \listun\ term \terminal{)} \\
& $|$ & \terminal{(} term \terminal{::} term \terminal{)} \\
& $|$ & \verb!<! term \verb!>! \terminal{Case}
term \terminal{of} \listzero\ term \terminal{end}
\\[1em]
name & ::= & \verb!_! \\
& $|$ & identifier
\end{tabular}
\end{center}
\hrulefill
\caption{Grammar of terms}
\label{fig:terms}
\end{figure}
\section{Commands}
The grammar of \minicoq's commands are given in
Figure~\ref{fig:commands}. All commands end with a dot.
\begin{figure}[htbp]
\hrulefill
\begin{center}
\begin{tabular}{lrl}
command & ::= & \terminal{Definition} identifier \terminal{:=} term. \\
& $|$ & \terminal{Definition} identifier \terminal{:} term
\terminal{:=} term. \\
& $|$ & \terminal{Parameter} identifier \terminal{:} term. \\
& $|$ & \terminal{Variable} identifier \terminal{:} term. \\
& $|$ & \terminal{Inductive} \terminal{[} \listzero\ param
\terminal{]} \listun\ inductive \sep\
\terminal{with}. \\
& $|$ & \terminal{Check} term.
\\[1em]
param & ::= & identifier
\\[1em]
inductive & ::= & identifier \terminal{:} term \terminal{:=}
\listzero\ constructor \sep\ \terminal{$|$}
\\[1em]
constructor & ::= & identifier \terminal{:} term
\end{tabular}
\end{center}
\hrulefill
\caption{Commands}
\label{fig:commands}
\end{figure}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
|
