diff options
Diffstat (limited to 'doc/RecTutorial/coqartmacros.tex')
| -rw-r--r-- | doc/RecTutorial/coqartmacros.tex | 180 |
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] |