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
|
\documentclass[12pt]{report}
\usepackage[utf8x]{inputenc}
%Warning: tipa declares many non-standard macros used by utf8x to
%interpret utf8 characters but extra packages might have to be added
%such as "textgreek" for Greek letters not already in tipa
%or "stmaryrd" for mathematical symbols.
%Utf8 codes missing a LaTeX interpretation can be defined by using
%\DeclareUnicodeCharacter{code}{interpretation}.
%Use coqdoc's option -p to add new packages or declarations.
\usepackage{tipa}
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\usepackage{url}
\begin{document}
\coqlibrary{Coqdoc.details}{Library }{Coqdoc.details}
\begin{coqdoccode}
\end{coqdoccode}
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.details.foo}{foo}{\coqdocdefinition{foo}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} := 3.\coqdoceol
\end{coqdoccode}
\begin{coqdoccode}
\coqdocemptyline
\end{coqdoccode}
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Fixpoint} \coqdef{Coqdoc.details.idnat}{idnat}{\coqdocdefinition{idnat}} (\coqdef{Coqdoc.details.x:1}{x}{\coqdocbinder{x}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} :=\coqdoceol
\coqdocindent{1.00em}
\coqdockw{match} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} \coqdocvar{x} \ensuremath{\Rightarrow} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} (\coqref{Coqdoc.details.idnat:2}{\coqdocdefinition{idnat}} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}})\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} 0 \ensuremath{\Rightarrow} 0\coqdoceol
\coqdocindent{1.00em}
\coqdockw{end}.\coqdoceol
\end{coqdoccode}
\begin{coqdoccode}
\end{coqdoccode}
\end{document}
|
