From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- doc/RecTutorial/recmacros.tex | 75 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 doc/RecTutorial/recmacros.tex (limited to 'doc/RecTutorial/recmacros.tex') diff --git a/doc/RecTutorial/recmacros.tex b/doc/RecTutorial/recmacros.tex new file mode 100644 index 00000000..0334553f --- /dev/null +++ b/doc/RecTutorial/recmacros.tex @@ -0,0 +1,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}} + + +%======================================= + -- cgit v1.2.3