summaryrefslogtreecommitdiff
path: root/doc/RecTutorial/coqartmacros.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/RecTutorial/coqartmacros.tex')
-rw-r--r--doc/RecTutorial/coqartmacros.tex180
1 files changed, 0 insertions, 180 deletions
diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex
deleted file mode 100644
index 6fb7534d..00000000
--- a/doc/RecTutorial/coqartmacros.tex
+++ /dev/null
@@ -1,180 +0,0 @@
-\usepackage{url}
-
-\newcommand{\variantspringer}[1]{#1}
-\newcommand{\marginok}[1]{\marginpar{\raggedright OK:#1}}
-\newcommand{\tab}{{\null\hskip1cm}}
-\newcommand{\Ltac}{\mbox{\emph{$\cal L$}tac}}
-\newcommand{\coq}{\mbox{\emph{Coq}}}
-\newcommand{\lcf}{\mbox{\emph{LCF}}}
-\newcommand{\hol}{\mbox{\emph{HOL}}}
-\newcommand{\pvs}{\mbox{\emph{PVS}}}
-\newcommand{\isabelle}{\mbox{\emph{Isabelle}}}
-\newcommand{\prolog}{\mbox{\emph{Prolog}}}
-\newcommand{\goalbar}{\tt{}============================\it}
-\newcommand{\gallina}{\mbox{\emph{Gallina}}}
-\newcommand{\joker}{\texttt{\_}}
-\newcommand{\eprime}{\(\e^{\prime}\)}
-\newcommand{\Ztype}{\citecoq{Z}}
-\newcommand{\propsort}{\citecoq{Prop}}
-\newcommand{\setsort}{\citecoq{Set}}
-\newcommand{\typesort}{\citecoq{Type}}
-\newcommand{\ocaml}{\mbox{\emph{OCAML}}}
-\newcommand{\haskell}{\mbox{\emph{Haskell}}}
-\newcommand{\why}{\mbox{\emph{Why}}}
-\newcommand{\Pascal}{\mbox{\emph{Pascal}}}
-
-\newcommand{\ml}{\mbox{\emph{ML}}}
-
-\newcommand{\scheme}{\mbox{\emph{Scheme}}}
-\newcommand{\lisp}{\mbox{\emph{Lisp}}}
-
-\newcommand{\implarrow}{\mbox{$\Rightarrow$}}
-\newcommand{\metavar}[1]{?#1}
-\newcommand{\notincoq}[1]{#1}
-\newcommand{\coqscope}[1]{\%#1}
-\newcommand{\arrow}{\mbox{$\rightarrow$}}
-\newcommand{\fleche}{\arrow}
-\newcommand{\funarrow}{\mbox{$\Rightarrow$}}
-\newcommand{\ltacarrow}{\funarrow}
-\newcommand{\coqand}{\mbox{\(\wedge\)}}
-\newcommand{\coqor}{\mbox{\(\vee\)}}
-\newcommand{\coqnot}{\mbox{\(\neg\)}}
-\newcommand{\hide}[1]{}
-\newcommand{\hidedots}[1]{...}
-\newcommand{\sig}[3]{\texttt{\{}#1\texttt{:}#2 \texttt{|} #3\texttt{\}}}
-\renewcommand{\neg}{\sim}
-\renewcommand{\marginpar}[1]{}
-
-\addtocounter{secnumdepth}{1}
-\providecommand{\og}{«}
-\providecommand{\fg}{»}
-
-
-\newcommand{\hard}{\mbox{\small *}}
-\newcommand{\xhard}{\mbox{\small **}}
-\newcommand{\xxhard}{\mbox{\small ***}}
-
-%%% Operateurs, etc.
-\newcommand{\impl}{\mbox{$\rightarrow$}}
-\newcommand{\appli}[2]{\mbox{\tt{#1 #2}}}
-\newcommand{\applis}[1]{\mbox{\texttt{#1}}}
-\newcommand{\abst}[3]{\mbox{\tt{fun #1:#2 \funarrow #3}}}
-\newcommand{\coqle}{\mbox{$\leq$}}
-\newcommand{\coqge}{\mbox{$\geq$}}
-\newcommand{\coqdiff}{\mbox{$\neq$}}
-\newcommand{\coqiff}{\mbox{$\leftrightarrow$}}
-\newcommand{\prodsym}{\mbox{\(\forall\,\)}}
-\newcommand{\exsym}{\mbox{\(\exists\,\)}}
-
-\newcommand{\substsign}{/}
-\newcommand{\subst}[3]{\mbox{#1\{#2\substsign{}#3\}}}
-\newcommand{\anoabst}[2]{\mbox{\tt[#1]#2}}
-\newcommand{\letin}[3]{\mbox{\tt let #1:=#2 in #3}}
-\newcommand{\prodep}[3]{\mbox{\tt \(\forall\,\)#1:#2,$\,$#3}}
-\newcommand{\prodplus}[2]{\mbox{\tt\(\forall\,\)$\,$#1,$\,$#2}}
-\newcommand{\dom}[1]{\textrm{dom}(#1)} % domaine d'un contexte (log function)
-\newcommand{\norm}[1]{\textrm{n}(#1)} % forme normale (log function)
-\newcommand{\coqZ}[1]{\mbox{\tt{`#1`}}}
-\newcommand{\coqnat}[1]{\mbox{\tt{#1}}}
-\newcommand{\coqcart}[2]{\mbox{\tt{#1*#2}}}
-\newcommand{\alphacong}{\mbox{$\,\cong_{\alpha}\,$}} % alpha-congruence
-\newcommand{\betareduc}{\mbox{$\,\rightsquigarrow_{\!\beta}$}\,} % beta reduction
-%\newcommand{\betastar}{\mbox{$\,\Rightarrow_{\!\beta}^{*}\,$}} % beta reduction
-\newcommand{\deltareduc}{\mbox{$\,\rightsquigarrow_{\!\delta}$}\,} % delta reduction
-\newcommand{\dbreduc}{\mbox{$\,\rightsquigarrow_{\!\delta\beta}$}\,} % delta,beta reduction
-\newcommand{\ireduc}{\mbox{$\,\rightsquigarrow_{\!\iota}$}\,} % delta,beta reduction
-
-
-% jugement de typage
-\newcommand{\these}{\boldsymbol{\large \vdash}}
-\newcommand{\disj}{\mbox{$\backslash/$}}
-\newcommand{\conj}{\mbox{$/\backslash$}}
-%\newcommand{\juge}[3]{\mbox{$#1 \boldsymbol{\vdash} #2 : #3 $}}
-\newcommand{\juge}[4]{\mbox{$#1,#2 \these #3 \boldsymbol{:} #4 $}}
-\newcommand{\smalljuge}[3]{\mbox{$#1 \these #2 \boldsymbol{:} #3 $}}
-\newcommand{\goal}[3]{\mbox{$#1,#2 \these^{\!\!\!?} #3 $}}
-\newcommand{\sgoal}[2]{\mbox{$#1\these^{\!\!\!\!?} #2 $}}
-\newcommand{\reduc}[5]{\mbox{$#1,#2 \these #3 \rhd_{#4}#5 $}}
-\newcommand{\convert}[5]{\mbox{$#1,#2 \these #3 =_{#4}#5 $}}
-\newcommand{\convorder}[5]{\mbox{$#1,#2 \these #3\leq _{#4}#5 $}}
-\newcommand{\wouff}[2]{\mbox{$\emph{WF}(#1)[#2]$}}
-
-
-%\newcommand{\mthese}{\underset{M}{\vdash}}
-\newcommand{\mthese}{\boldsymbol{\vdash}_{\!\!M}}
-\newcommand{\type}{\boldsymbol{:}}
-
-% jugement absolu
-
-%\newcommand{\ajuge}[2]{\mbox{$ \boldsymbol{\vdash} #1 : #2 $}}
-\newcommand{\ajuge}[2]{\mbox{$\these #1 \boldsymbol{:} #2 $}}
-
-%%% logique minimale
-\newcommand{\propzero}{\mbox{$P_0$}} % types de Fzero
-
-%%% logique propositionnelle classique
-\newcommand {\ff}{\boldsymbol{f}} % faux
-\newcommand {\vv}{\boldsymbol{t}} % vrai
-
-\newcommand{\verite}{\mbox{$\cal{B}$}} % {\ff,\vv}
-\newcommand{\sequ}[2]{\mbox{$#1 \vdash #2 $}} % sequent
-\newcommand{\strip}[1]{#1^o} % enlever les variables d'un contexte
-
-
-
-%%% tactiques
-\newcommand{\decomp}{\delta} % decomposition
-\newcommand{\recomp}{\rho} % recomposition
-
-%%% divers
-\newcommand{\cqfd}{\mbox{\textbf{cqfd}}}
-\newcommand{\fail}{\mbox{\textbf{F}}}
-\newcommand{\succes}{\mbox{$\blacksquare$}}
-%%% Environnements
-
-
-%% Fzero
-\newcommand{\con}{\mbox{$\cal C$}}
-\newcommand{\var}{\mbox{$\cal V$}}
-
-\newcommand{\atomzero}{\mbox{${\cal A}_0$}} % types de base de Fzero
-\newcommand{\typezero}{\mbox{${\cal T}_0$}} % types de Fzero
-\newcommand{\termzero}{\mbox{$\Lambda_0$}} % termes de Fzero
-\newcommand{\conzero}{\mbox{$\cal C_0$}} % contextes de Fzero
-
-\newcommand{\buts}{\mbox{$\cal B$}} % buts
-
-%%% for drawing terms
-% abstraction [x:t]e
-\newcommand{\PicAbst}[3]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}\chunk{#3}%
- \end{bundle}}
-
-% the same in DeBruijn form
-\newcommand{\PicDbj}[2]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}
- \end{bundle}}
-
-
-% applications
-\newcommand{\PicAppl}[2]{\begin{bundle}{\bf appl}\chunk{#1}\chunk{#2}%
- \end{bundle}}
-
-% variables
-\newcommand{\PicVar}[1]{\begin{bundle}{\bf var}\chunk{#1}
- \end{bundle}}
-
-% constantes
-\newcommand{\PicCon}[1]{\begin{bundle}{\bf const}\chunk{#1}\end{bundle}}
-
-% arrows
-\newcommand{\PicImpl}[2]{\begin{bundle}{\impl}\chunk{#1}\chunk{#2}%
- \end{bundle}}
-
-
-
-%%%% scripts coq
-\newcommand{\prompt}{\mbox{\sl Coq $<\;$}}
-\newcommand{\natquicksort}{\texttt{nat\_quicksort}}
-\newcommand{\citecoq}[1]{\mbox{\texttt{#1}}}
-\newcommand{\safeit}{\it}
-\newtheorem{remarque}{Remark}[section]
-%\newtheorem{definition}{Definition}[chapter]