← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to dev/doc/minicoq.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

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