diff options
Diffstat (limited to 'doc/common/macros.tex')
| -rwxr-xr-x | doc/common/macros.tex | 529 |
1 files changed, 0 insertions, 529 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex deleted file mode 100755 index d745f34a..00000000 --- a/doc/common/macros.tex +++ /dev/null @@ -1,529 +0,0 @@ -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% 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: |