aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/RecTutorial/recmacros.tex
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}}


%=======================================