diff options
Diffstat (limited to 'doc/common/macros.tex')
| -rwxr-xr-x | doc/common/macros.tex | 529 |
1 files changed, 529 insertions, 0 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex new file mode 100755 index 00000000..d745f34a --- /dev/null +++ b/doc/common/macros.tex @@ -0,0 +1,529 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% MACROS FOR THE REFERENCE MANUAL OF COQ % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% For commentaries (define \com as {} for the release manual) +%\newcommand{\com}[1]{{\it(* #1 *)}} +%\newcommand{\com}[1]{} + +%%OPTIONS for HACHA +%\renewcommand{\cuttingunit}{section} + + +%BEGIN LATEX +\newenvironment{centerframe}% +{\bgroup +\dimen0=\textwidth +\advance\dimen0 by -2\fboxrule +\advance\dimen0 by -2\fboxsep +\setbox0=\hbox\bgroup +\begin{minipage}{\dimen0}% +\begin{center}}% +{\end{center}% +\end{minipage}\egroup +\centerline{\fbox{\box0}}\egroup +} +%END LATEX +%HEVEA \newenvironment{centerframe}{\begin{center}}{\end{center}} + +%HEVEA \renewcommand{\vec}[1]{\mathbf{#1}} +%\renewcommand{\ominus}{-} % Hevea does a good job translating these commands +%\renewcommand{\oplus}{+} +%\renewcommand{\otimes}{\times} +%\newcommand{\land}{\wedge} +%\newcommand{\lor}{\vee} +%HEVEA \renewcommand{\k}[1]{#1} % \k{a} is supposed to produce a with a little stroke +%HEVEA \newcommand{\phantom}[1]{\qquad} + +%%%%%%%%%%%%%%%%%%%%%%% +% Formatting commands % +%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\ErrMsg}{\medskip \noindent {\bf Error message: }} +\newcommand{\ErrMsgx}{\medskip \noindent {\bf Error messages: }} +\newcommand{\variant}{\medskip \noindent {\bf Variant: }} +\newcommand{\variants}{\medskip \noindent {\bf Variants: }} +\newcommand{\SeeAlso}{\medskip \noindent {\bf See also: }} +\newcommand{\Rem}{\medskip \noindent {\bf Remark: }} +\newcommand{\Rems}{\medskip \noindent {\bf Remarks: }} +\newcommand{\Example}{\medskip \noindent {\bf Example: }} +\newcommand{\examples}{\medskip \noindent {\bf Examples: }} +\newcommand{\Warning}{\medskip \noindent {\bf Warning: }} +\newcommand{\Warns}{\medskip \noindent {\bf Warnings: }} +\newcounter{ex} +\newcommand{\firstexample}{\setcounter{ex}{1}} +\newcommand{\example}[1]{ +\medskip \noindent \textbf{Example \arabic{ex}: }\textit{#1} +\addtocounter{ex}{1}} + +\newenvironment{Variant}{\variant\begin{enumerate}}{\end{enumerate}} +\newenvironment{Variants}{\variants\begin{enumerate}}{\end{enumerate}} +\newenvironment{ErrMsgs}{\ErrMsgx\begin{enumerate}}{\end{enumerate}} +\newenvironment{Remarks}{\Rems\begin{enumerate}}{\end{enumerate}} +\newenvironment{Warnings}{\Warns\begin{enumerate}}{\end{enumerate}} +\newenvironment{Examples}{\medskip\noindent{\bf Examples:} +\begin{enumerate}}{\end{enumerate}} + +%\newcommand{\bd}{\noindent\bf} +%\newcommand{\sbd}{\vspace{8pt}\noindent\bf} +%\newcommand{\sdoll}[1]{\begin{small}$ #1~ $\end{small}} +%\newcommand{\sdollnb}[1]{\begin{small}$ #1 $\end{small}} +\newcommand{\kw}[1]{\textsf{#1}} +%\newcommand{\spec}[1]{\{\,#1\,\}} + +% Building regular expressions +\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}} +%\newcommand{\zeroonemany}[1]{$\{$#1$\}$*} +%\newcommand{\onemany}[1]{$\{$#1$\}$+} +\newcommand{\nelist}[2]{{#1} {\tt #2}~{\ldots}~{\tt #2} {#1}} +\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2}~{\ldots}~{\tt #2} {#1}{\sl ]}} +\newcommand{\nelistwithoutblank}[2]{#1{\tt #2}\ldots{\tt #2}#1} +\newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\ldots{\tt #2}#1$]$} + +% Used for RefMan-gal +%\newcommand{\ml}[1]{\hbox{\tt{#1}}} +%\newcommand{\op}{\,|\,} + +%%%%%%%%%%%%%%%%%%%%%%%% +% Trademarks and so on % +%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\Coq}{\textsc{Coq}} +\newcommand{\gallina}{\textsc{Gallina}} +\newcommand{\Gallina}{\textsc{Gallina}} +\newcommand{\CoqIDE}{\textsc{CoqIDE}} +\newcommand{\ocaml}{\textsc{Objective Caml}} +\newcommand{\camlpppp}{\textsc{Camlp4}} +\newcommand{\emacs}{\textsc{GNU Emacs}} +\newcommand{\CIC}{\pCIC} +\newcommand{\pCIC}{p\textsc{Cic}} +\newcommand{\iCIC}{\textsc{Cic}} +\newcommand{\FW}{\ensuremath{F_{\omega}}} +\newcommand{\Program}{\textsc{Program}} +\newcommand{\Russell}{\textsc{Russell}} +\newcommand{\PVS}{\textsc{PVS}} +%\newcommand{\bn}{{\sf BNF}} + +%%%%%%%%%%%%%%%%%%% +% Name of tactics % +%%%%%%%%%%%%%%%%%%% + +%\newcommand{\Natural}{\mbox{\tt Natural}} + +%%%%%%%%%%%%%%%%% +% \rm\sl series % +%%%%%%%%%%%%%%%%% + +\newcommand{\nterm}[1]{\textrm{\textsl{#1}}} + +\newcommand{\qstring}{\nterm{string}} + +%% New syntax specific entries +\newcommand{\annotation}{\nterm{annotation}} +\newcommand{\assums}{\nterm{assums}} % vernac +\newcommand{\simpleassums}{\nterm{simple\_assums}} % assumptions +\newcommand{\binder}{\nterm{binder}} +\newcommand{\binders}{\nterm{binders}} +\newcommand{\caseitems}{\nterm{match\_items}} +\newcommand{\caseitem}{\nterm{match\_item}} +\newcommand{\eqn}{\nterm{equation}} +\newcommand{\ifitem}{\nterm{dep\_ret\_type}} +\newcommand{\convclause}{\nterm{conversion\_clause}} +\newcommand{\occclause}{\nterm{occurrence\_clause}} +\newcommand{\occgoalset}{\nterm{goal\_occurrences}} +\newcommand{\atoccurrences}{\nterm{at\_occurrences}} +\newcommand{\occlist}{\nterm{occurrences}} +\newcommand{\params}{\nterm{params}} % vernac +\newcommand{\returntype}{\nterm{return\_type}} +\newcommand{\idparams}{\nterm{ident\_with\_params}} +\newcommand{\statkwd}{\nterm{assertion\_keyword}} % vernac +\newcommand{\termarg}{\nterm{arg}} + +\newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}} +\newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}} + + +\newcommand{\Fwterm}{\nterm{Fwterm}} +\newcommand{\Index}{\nterm{index}} +\newcommand{\abbrev}{\nterm{abbreviation}} +\newcommand{\atomictac}{\nterm{atomic\_tactic}} +\newcommand{\bindinglist}{\nterm{bindings\_list}} +\newcommand{\cast}{\nterm{cast}} +\newcommand{\cofixpointbodies}{\nterm{cofix\_bodies}} +\newcommand{\cofixpointbody}{\nterm{cofix\_body}} +\newcommand{\commandtac}{\nterm{tactic\_invocation}} +\newcommand{\constructor}{\nterm{constructor}} +\newcommand{\convtactic}{\nterm{conv\_tactic}} +\newcommand{\assumptionkeyword}{\nterm{assumption\_keyword}} +\newcommand{\assumption}{\nterm{assumption}} +\newcommand{\definition}{\nterm{definition}} +\newcommand{\digit}{\nterm{digit}} +\newcommand{\exteqn}{\nterm{ext\_eqn}} +\newcommand{\field}{\nterm{field}} +\newcommand{\firstletter}{\nterm{first\_letter}} +\newcommand{\fixpg}{\nterm{fix\_pgm}} +\newcommand{\fixpointbodies}{\nterm{fix\_bodies}} +\newcommand{\fixpointbody}{\nterm{fix\_body}} +\newcommand{\fixpoint}{\nterm{fixpoint}} +\newcommand{\flag}{\nterm{flag}} +\newcommand{\form}{\nterm{form}} +\newcommand{\entry}{\nterm{entry}} +\newcommand{\proditem}{\nterm{production\_item}} +\newcommand{\taclevel}{\nterm{tactic\_level}} +\newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} +\newcommand{\scope}{\nterm{scope}} +\newcommand{\delimkey}{\nterm{key}} +\newcommand{\optscope}{\nterm{opt\_scope}} +\newcommand{\declnotation}{\nterm{decl\_notation}} +\newcommand{\symbolentry}{\nterm{symbol}} +\newcommand{\modifiers}{\nterm{modifiers}} +\newcommand{\localdef}{\nterm{local\_def}} +\newcommand{\localdecls}{\nterm{local\_decls}} +\newcommand{\ident}{\nterm{ident}} +\newcommand{\accessident}{\nterm{access\_ident}} +\newcommand{\possiblybracketedident}{\nterm{possibly\_bracketed\_ident}} +\newcommand{\inductivebody}{\nterm{ind\_body}} +\newcommand{\inductive}{\nterm{inductive}} +\newcommand{\naturalnumber}{\nterm{natural}} +\newcommand{\integer}{\nterm{integer}} +\newcommand{\multpattern}{\nterm{mult\_pattern}} +\newcommand{\mutualcoinductive}{\nterm{mutual\_coinductive}} +\newcommand{\mutualinductive}{\nterm{mutual\_inductive}} +\newcommand{\nestedpattern}{\nterm{nested\_pattern}} +\newcommand{\name}{\nterm{name}} +\newcommand{\num}{\nterm{num}} +\newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching +\newcommand{\orpattern}{\nterm{or\_pattern}} +\newcommand{\intropattern}{\nterm{intro\_pattern}} +\newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}} +\newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}} +\newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes +\newcommand{\pat}{\nterm{pat}} +\newcommand{\pgs}{\nterm{pgms}} +\newcommand{\pg}{\nterm{pgm}} +%BEGIN LATEX +\newcommand{\proof}{\nterm{proof}} +%END LATEX +%HEVEA \renewcommand{\proof}{\nterm{proof}} +\newcommand{\record}{\nterm{record}} +\newcommand{\rewrule}{\nterm{rewriting\_rule}} +\newcommand{\sentence}{\nterm{sentence}} +\newcommand{\simplepattern}{\nterm{simple\_pattern}} +\newcommand{\sort}{\nterm{sort}} +\newcommand{\specif}{\nterm{specif}} +\newcommand{\assertion}{\nterm{assertion}} +\newcommand{\str}{\nterm{string}} +\newcommand{\subsequentletter}{\nterm{subsequent\_letter}} +\newcommand{\switch}{\nterm{switch}} +\newcommand{\messagetoken}{\nterm{message\_token}} +\newcommand{\tac}{\nterm{tactic}} +\newcommand{\terms}{\nterm{terms}} +\newcommand{\term}{\nterm{term}} +\newcommand{\module}{\nterm{module}} +\newcommand{\modexpr}{\nterm{module\_expression}} +\newcommand{\modtype}{\nterm{module\_type}} +\newcommand{\onemodbinding}{\nterm{module\_binding}} +\newcommand{\modbindings}{\nterm{module\_bindings}} +\newcommand{\qualid}{\nterm{qualid}} +\newcommand{\qualidorstring}{\nterm{qualid\_or\_string}} +\newcommand{\class}{\nterm{class}} +\newcommand{\dirpath}{\nterm{dirpath}} +\newcommand{\typedidents}{\nterm{typed\_idents}} +\newcommand{\type}{\nterm{type}} +\newcommand{\vref}{\nterm{ref}} +\newcommand{\zarithformula}{\nterm{zarith\_formula}} +\newcommand{\zarith}{\nterm{zarith}} +\newcommand{\ltac}{\mbox{${\cal L}_{tac}$}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% \mbox{\sf } series for roman text in maths formulas % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\alors}{\mbox{\textsf{then}}} +\newcommand{\alter}{\mbox{\textsf{alter}}} +\newcommand{\bool}{\mbox{\textsf{bool}}} +\newcommand{\conc}{\mbox{\textsf{conc}}} +\newcommand{\cons}{\mbox{\textsf{cons}}} +\newcommand{\consf}{\mbox{\textsf{consf}}} +\newcommand{\emptyf}{\mbox{\textsf{emptyf}}} +\newcommand{\EqSt}{\mbox{\textsf{EqSt}}} +\newcommand{\false}{\mbox{\textsf{false}}} +\newcommand{\filter}{\mbox{\textsf{filter}}} +\newcommand{\forest}{\mbox{\textsf{forest}}} +\newcommand{\from}{\mbox{\textsf{from}}} +\newcommand{\hd}{\mbox{\textsf{hd}}} +\newcommand{\Length}{\mbox{\textsf{Length}}} +\newcommand{\length}{\mbox{\textsf{length}}} +\newcommand{\LengthA}{\mbox {\textsf{Length\_A}}} +\newcommand{\List}{\mbox{\textsf{List}}} +\newcommand{\ListA}{\mbox{\textsf{List\_A}}} +\newcommand{\LNil}{\mbox{\textsf{Lnil}}} +\newcommand{\LCons}{\mbox{\textsf{Lcons}}} +\newcommand{\nat}{\mbox{\textsf{nat}}} +\newcommand{\nO}{\mbox{\textsf{O}}} +\newcommand{\nS}{\mbox{\textsf{S}}} +\newcommand{\node}{\mbox{\textsf{node}}} +\newcommand{\Nil}{\mbox{\textsf{nil}}} +\newcommand{\Prop}{\mbox{\textsf{Prop}}} +\newcommand{\Set}{\mbox{\textsf{Set}}} +\newcommand{\si}{\mbox{\textsf{if}}} +\newcommand{\sinon}{\mbox{\textsf{else}}} +\newcommand{\Str}{\mbox{\textsf{Stream}}} +\newcommand{\tl}{\mbox{\textsf{tl}}} +\newcommand{\tree}{\mbox{\textsf{tree}}} +\newcommand{\true}{\mbox{\textsf{true}}} +\newcommand{\Type}{\mbox{\textsf{Type}}} +\newcommand{\unfold}{\mbox{\textsf{unfold}}} +\newcommand{\zeros}{\mbox{\textsf{zeros}}} + +%%%%%%%%% +% Misc. % +%%%%%%%%% +\newcommand{\T}{\texttt{T}} +\newcommand{\U}{\texttt{U}} +\newcommand{\real}{\textsf{Real}} +\newcommand{\Data}{\textit{Data}} +\newcommand{\In} {{\textbf{in }}} +\newcommand{\AND} {{\textbf{and}}} +\newcommand{\If}{{\textbf{if }}} +\newcommand{\Else}{{\textbf{else }}} +\newcommand{\Then} {{\textbf{then }}} +%\newcommand{\Let}{{\textbf{let }}} % looks like this is never used +\newcommand{\Where}{{\textbf{where rec }}} +\newcommand{\Function}{{\textbf{function }}} +\newcommand{\Rec}{{\textbf{rec }}} +%\newcommand{\cn}{\centering} +\newcommand{\nth}{\mbox{$^{\mbox{\scriptsize th}}$}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Math commands and symbols % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\la}{\leftarrow} +\newcommand{\ra}{\rightarrow} +\newcommand{\Ra}{\Rightarrow} +\newcommand{\rt}{\Rightarrow} +\newcommand{\lla}{\longleftarrow} +\newcommand{\lra}{\longrightarrow} +\newcommand{\Llra}{\Longleftrightarrow} +\newcommand{\mt}{\mapsto} +\newcommand{\ov}{\overrightarrow} +\newcommand{\wh}{\widehat} +\newcommand{\up}{\uparrow} +\newcommand{\dw}{\downarrow} +\newcommand{\nr}{\nearrow} +\newcommand{\se}{\searrow} +\newcommand{\sw}{\swarrow} +\newcommand{\nw}{\nwarrow} +\newcommand{\mto}{,} + +\newcommand{\vm}[1]{\vspace{#1em}} +\newcommand{\vx}[1]{\vspace{#1ex}} +\newcommand{\hm}[1]{\hspace{#1em}} +\newcommand{\hx}[1]{\hspace{#1ex}} +\newcommand{\sm}{\mbox{ }} +\newcommand{\mx}{\mbox} + +%\newcommand{\nq}{\neq} +%\newcommand{\eq}{\equiv} +\newcommand{\fa}{\forall} +%\newcommand{\ex}{\exists} +\newcommand{\impl}{\rightarrow} +%\newcommand{\Or}{\vee} +%\newcommand{\And}{\wedge} +\newcommand{\ms}{\models} +\newcommand{\bw}{\bigwedge} +\newcommand{\ts}{\times} +\newcommand{\cc}{\circ} +%\newcommand{\es}{\emptyset} +%\newcommand{\bs}{\backslash} +\newcommand{\vd}{\vdash} +%\newcommand{\lan}{{\langle }} +%\newcommand{\ran}{{\rangle }} + +%\newcommand{\al}{\alpha} +\newcommand{\bt}{\beta} +%\newcommand{\io}{\iota} +\newcommand{\lb}{\lambda} +%\newcommand{\sg}{\sigma} +%\newcommand{\sa}{\Sigma} +%\newcommand{\om}{\Omega} +%\newcommand{\tu}{\tau} + +%%%%%%%%%%%%%%%%%%%%%%%%% +% Custom maths commands % +%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\sumbool}[2]{\{#1\}+\{#2\}} +\newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3} +\newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2} +\newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}} +\newcommand{\WFE}[1]{\WF{E}{#1}} +\newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}} +\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} +\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} + +\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} +\newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\cal W\!F}(#2)}} +\newcommand{\WS}[3]{\ensuremath{#1[] \vdash #2 <: #3}} +\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} + +\newcommand{\WTRED}[5]{\mbox{$#1[#2] \vdash #3 #4 #5$}} +\newcommand{\WTERED}[4]{\mbox{$E[#1] \vdash #2 #3 #4$}} +\newcommand{\WTELECONV}[3]{\WTERED{#1}{#2}{\leconvert}{#3}} +\newcommand{\WTEGRED}[3]{\WTERED{\Gamma}{#1}{#2}{#3}} +\newcommand{\WTECONV}[3]{\WTERED{#1}{#2}{\convert}{#3}} +\newcommand{\WTEGCONV}[2]{\WTERED{\Gamma}{#1}{\convert}{#2}} +\newcommand{\WTEGLECONV}[2]{\WTERED{\Gamma}{#1}{\leconvert}{#2}} + +\newcommand{\lab}[1]{\mathit{labels}(#1)} +\newcommand{\dom}[1]{\mathit{dom}(#1)} + +\newcommand{\CI}[2]{\mbox{$\{#1\}^{#2}$}} +\newcommand{\CIP}[3]{\mbox{$\{#1\}_{#2}^{#3}$}} +\newcommand{\CIPV}[1]{\CIP{#1}{I_1.. I_k}{P_1.. P_k}} +\newcommand{\CIPI}[1]{\CIP{#1}{I}{P}} +\newcommand{\CIF}[1]{\mbox{$\{#1\}_{f_1.. f_n}$}} +%BEGIN LATEX +\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(\begin{array}[t]{@{}l}#2:=#3 + \,)\end{array}$}} +\newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{@{}l@{}}#3:=#4 + \,)\end{array}$}} +%END LATEX +%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}} +%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}} + +\newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4 + \,)\end{array}$}} +\newcommand{\Indpstr}[6]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4 + \,)/{#6}\end{array}$}} +\newcommand{\Def}[4]{\mbox{{\sf Def}$(#1)(#2:=#3:#4)$}} +\newcommand{\Assum}[3]{\mbox{{\sf Assum}$(#1)(#2:#3)$}} +\newcommand{\Match}[3]{\mbox{$<\!#1\!>\!{\mbox{\tt Match}}~#2~{\mbox{\tt with}}~#3~{\mbox{\tt end}}$}} +\newcommand{\Case}[3]{\mbox{$\kw{case}(#2,#1,#3)$}} +\newcommand{\match}[3]{\mbox{$\kw{match}~ #2 ~\kw{with}~ #3 ~\kw{end}$}} +\newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}} +\newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}} +\newcommand{\With}[2]{\mbox{\tt ~with~}} +\newcommand{\subst}[3]{#1\{#2/#3\}} +\newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}} +\newcommand{\Sort}{\mbox{$\cal S$}} +\newcommand{\convert}{=_{\beta\delta\iota\zeta}} +\newcommand{\leconvert}{\leq_{\beta\delta\iota\zeta}} +\newcommand{\NN}{\mathbb{N}} +\newcommand{\inference}[1]{$${#1}$$} + +\newcommand{\compat}[2]{\mbox{$[#1|#2]$}} +\newcommand{\tristackrel}[3]{\mathrel{\mathop{#2}\limits_{#3}^{#1}}} + +\newcommand{\Impl}{{\it Impl}} +\newcommand{\elem}{{\it e}} +\newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}\,\zeroone{:={#3}})} +\newcommand{\ModS}[2]{{\sf Mod}({#1}:{#2})} +\newcommand{\ModType}[2]{{\sf ModType}({#1}:={#2})} +\newcommand{\ModA}[2]{{\sf ModA}({#1}=={#2})} +\newcommand{\functor}[3]{\ensuremath{{\sf Functor}(#1:#2)\;#3}} +\newcommand{\funsig}[3]{\ensuremath{{\sf Funsig}(#1:#2)\;#3}} +\newcommand{\sig}[1]{\ensuremath{{\sf Sig}~#1~{\sf End}}} +\newcommand{\struct}[1]{\ensuremath{{\sf Struct}~#1~{\sf End}}} +\newcommand{\structe}[1]{\ensuremath{ + {\sf Struct}~\elem_1;\ldots;\elem_i;#1;\elem_{i+2};\ldots + ;\elem_n~{\sf End}}} +\newcommand{\structes}[2]{\ensuremath{ + {\sf Struct}~\elem_1;\ldots;\elem_i;#1;\elem_{i+2}\{#2\} + ;\ldots;\elem_n\{#2\}~{\sf End}}} +\newcommand{\with}[3]{\ensuremath{#1~{\sf with}~#2 := #3}} + +\newcommand{\Spec}{{\it Spec}} +\newcommand{\ModSEq}[3]{{\sf Mod}({#1}:{#2}:={#3})} + + +%\newbox\tempa +%\newbox\tempb +%\newdimen\tempc +%\newcommand{\mud}[1]{\hfil $\displaystyle{\mathstrut #1}$\hfil} +%\newcommand{\rig}[1]{\hfil $\displaystyle{#1}$} +% \newcommand{\irulehelp}[3]{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}% +% \setbox\tempb=\vbox{\halign{##\cr +% \mud{#1}\cr +% \noalign{\vskip\the\lineskip} +% \noalign{\hrule height 0pt} +% \rig{\vbox to 0pt{\vss\hbox to 0pt{${\; #3}$\hss}\vss}}\cr +% \noalign{\hrule} +% \noalign{\vskip\the\lineskip} +% \mud{\copy\tempa}\cr}} +% \tempc=\wd\tempb +% \advance\tempc by \wd\tempa +% \divide\tempc by 2 } +% \newcommand{\irule}[3]{{\irulehelp{#1}{#2}{#3} +% \hbox to \wd\tempa{\hss \box\tempb \hss}}} + +\newcommand{\sverb}[1]{{\tt #1}} +\newcommand{\mover}[2]{{#1\over #2}} +\newcommand{\jd}[2]{#1 \vdash #2} +\newcommand{\mathline}[1]{\[#1\]} +\newcommand{\zrule}[2]{#2: #1} +\newcommand{\orule}[3]{#3: {\mover{#1}{#2}}} +\newcommand{\trule}[4]{#4: \mover{#1 \qquad #2} {#3}} +\newcommand{\thrule}[5]{#5: {\mover{#1 \qquad #2 \qquad #3}{#4}}} + + + +% placement of figures + +%BEGIN LATEX +\renewcommand{\topfraction}{.99} +\renewcommand{\bottomfraction}{.99} +\renewcommand{\textfraction}{.01} +\renewcommand{\floatpagefraction}{.9} +%END LATEX + +% Macros Bruno pour description de la syntaxe + +\def\bfbar{\ensuremath{|\hskip -0.22em{}|\hskip -0.24em{}|}} +\def\TERMbar{\bfbar} +\def\TERMbarbar{\bfbar\bfbar} + + +%% Macros pour les grammaires +\def\GR#1{\text{\large(}#1\text{\large)}} +\def\NT#1{\langle\textit{#1}\rangle} +\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}} +\def\TERM#1{{\bf\textrm{\bf #1}}} +%\def\TERM#1{{\bf\textsf{#1}}} +\def\KWD#1{\TERM{#1}} +\def\ETERM#1{\TERM{#1}} +\def\CHAR#1{\TERM{#1}} + +\def\STAR#1{#1*} +\def\STARGR#1{\GR{#1}*} +\def\PLUS#1{#1+} +\def\PLUSGR#1{\GR{#1}+} +\def\OPT#1{#1?} +\def\OPTGR#1{\GR{#1}?} +%% Tableaux de definition de non-terminaux +\newenvironment{cadre} + {\begin{array}{|c|}\hline\\} + {\\\\\hline\end{array}} +\newenvironment{rulebox} + {$$\begin{cadre}\begin{array}{r@{~}c@{~}l@{}l@{}r}} + {\end{array}\end{cadre}$$} +\def\DEFNT#1{\NT{#1} & ::= &} +\def\EXTNT#1{\NT{#1} & ::= & ... \\&|&} +\def\RNAME#1{(\textsc{#1})} +\def\SEPDEF{\\\\} +\def\nlsep{\\&|&} +\def\nlcont{\\&&} +\newenvironment{rules} + {\begin{center}\begin{rulebox}} + {\end{rulebox}\end{center}} + +% $Id: macros.tex 13091 2010-06-08 13:56:19Z herbelin $ + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: |