blob: 0334553f27b86f57a90bfd7de2e33b80a40ae623 (
plain)
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
|
%===================================
% Style of the document
%===================================
%\newtheorem{example}{Example}[section]
%\newtheorem{exercise}{Exercise}[section]
\newcommand{\comentario}[1]{\texttt{#1}}
%===================================
% Keywords
%===================================
\newcommand{\Prop}{\texttt{Prop}}
\newcommand{\Set}{\texttt{Set}}
\newcommand{\Type}{\texttt{Type}}
\newcommand{\true}{\texttt{true}}
\newcommand{\false}{\texttt{false}}
\newcommand{\Lth}{\texttt{Lth}}
\newcommand{\Nat}{\texttt{nat}}
\newcommand{\nat}{\texttt{nat}}
\newcommand{\Z} {\texttt{O}}
\newcommand{\SUCC}{\texttt{S}}
\newcommand{\pred}{\texttt{pred}}
\newcommand{\False}{\texttt{False}}
\newcommand{\True}{\texttt{True}}
\newcommand{\I}{\texttt{I}}
\newcommand{\natind}{\texttt{nat\_ind}}
\newcommand{\natrec}{\texttt{nat\_rec}}
\newcommand{\natrect}{\texttt{nat\_rect}}
\newcommand{\eqT}{\texttt{eqT}}
\newcommand{\identityT}{\texttt{identityT}}
\newcommand{\map}{\texttt{map}}
\newcommand{\iterates}{\texttt{iterates}}
%===================================
% Numbering
%===================================
\newtheorem{definition}{Definition}[section]
\newtheorem{example}{Example}[section]
%===================================
% Judgements
%===================================
\newcommand{\JM}[2]{\ensuremath{#1 : #2}}
%===================================
% Expressions
%===================================
\newcommand{\Case}[3][]{\ensuremath{#1\textsf{Case}~#2~\textsf of}~#3~\textsf{end}}
%=======================================
\newcommand{\snreglados} [3] {\begin{tabular}{c} \ensuremath{#1} \\[2pt]
\ensuremath{#2}\\ \hline \ensuremath{#3} \end{tabular}}
\newcommand{\snregla} [2] {\begin{tabular}{c}
\ensuremath{#1}\\ \hline \ensuremath{#2} \end{tabular}}
%=======================================
|
