summaryrefslogtreecommitdiff
path: root/dev/doc/minicoq.tex
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /dev/doc/minicoq.tex
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'dev/doc/minicoq.tex')
-rw-r--r--dev/doc/minicoq.tex98
1 files changed, 98 insertions, 0 deletions
diff --git a/dev/doc/minicoq.tex b/dev/doc/minicoq.tex
new file mode 100644
index 00000000..a34b03a4
--- /dev/null
+++ b/dev/doc/minicoq.tex
@@ -0,0 +1,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: