macros.tex

% Symbols

\newcommand{\symadd}{+}
\newcommand{\symbrand}{b}
\newcommand{\symcons}{cons}
\newcommand{\symconf}{F}
\newcommand{\symconm}{F}
\newcommand{\symconmt}{E}
\newcommand{\symcont}{E}
\newcommand{\symconu}{U}
\newcommand{\symcs}{k}
\newcommand{\symcsvar}{y}
\newcommand{\symenv}{\Gamma}
\newcommand{\symlumpeq}{\doteq}
\newcommand{\symempty}{\emptyset}
\newcommand{\symexp}{e}
\newcommand{\symext}{,}
\newcommand{\symhasty}{:}
\newcommand{\symfield}{c}
\newcommand{\symfor}{\forall}
\newcommand{\symfun}{\rightarrow}
\newcommand{\symhd}{hd}
\newcommand{\symhm}{hm}
\newcommand{\symholeh}{\ensuremath{[\,]\langh}\xspace}
\newcommand{\symholem}{\ensuremath{[\,]\langm}\xspace}
\newcommand{\symholes}{\ensuremath{[\,]\langs}\xspace}
\newcommand{\symhs}{hs}
\newcommand{\symif}{if0}
\newcommand{\symjud}{\vdash}
\newcommand{\symjudh}{\symjud\langh}
\newcommand{\symjudm}{\symjud\langm}
\newcommand{\symjuds}{\symjud\langs}
\newcommand{\symlangh}{H}
\newcommand{\symlangm}{M}
\newcommand{\symlangs}{S}
\newcommand{\symlump}{L}
\newcommand{\symmh}{mh}
\newcommand{\symms}{ms}
\newcommand{\symnat}{N}
\newcommand{\symnil}{nil}
\newcommand{\sympnull}{null?}
\newcommand{\symnum}{n}
\newcommand{\symop}{a}
\newcommand{\sympred}{p}
\newcommand{\sympfun}{fun?}
\newcommand{\symplist}{list?}
\newcommand{\sympnum}{num?}
\newcommand{\symred}{\rightarrow}
\newcommand{\symsh}{sh}
\newcommand{\symsm}{sm}
\newcommand{\symstr}{string}
\newcommand{\symsub}{-}
\newcommand{\symtl}{tl}
\newcommand{\symtst}{TST}
\newcommand{\symty}{t}
\newcommand{\symtyvar}{y}
\newcommand{\symvalf}{f}
\newcommand{\symvalt}{v}
\newcommand{\symvalu}{u}
\newcommand{\symvar}{x}
\newcommand{\symwrong}{wrong}

% Languages

\newcommand{\langh}{\formlang{\symlangh}}
\newcommand{\langm}{\formlang{\symlangm}}
\newcommand{\langs}{\formlang{\symlangs}}

% Variables

\newcommand{\varbrand}{\ensuremath{\symbrand}\xspace}

\newcommand{\varconm}{\ensuremath{\mathscr{\symconm}\xspace}}
\newcommand{\varconmt}{\ensuremath{\mathscr{\symconmt}\xspace}}

\newcommand{\varcont}{\ensuremath{\symcont}\xspace}
\newcommand{\varconth}{\ensuremath{\varcont\langh}\xspace}
\newcommand{\varcontm}{\ensuremath{\varcont\langm}\xspace}
\newcommand{\varconts}{\ensuremath{\varcont\langs}\xspace}

\newcommand{\varvalt}{\ensuremath{\symvalt}\xspace}
\newcommand{\varvalth}{\ensuremath{\varvalt\langh}\xspace}
\newcommand{\varvaltm}{\ensuremath{\varvalt\langm}\xspace}
\newcommand{\varvalts}{\ensuremath{\varvalt\langs}\xspace}

\newcommand{\varconf}{\ensuremath{\symconf}\xspace}
\newcommand{\varconfh}{\ensuremath{\varconf\langh}\xspace}
\newcommand{\varconfm}{\ensuremath{\varconf\langm}\xspace}
\newcommand{\varconfs}{\ensuremath{\varconf\langs}\xspace}

\newcommand{\varconu}{\ensuremath{\symconu}\xspace}
\newcommand{\varconum}{\ensuremath{\varconu\langm}\xspace}
\newcommand{\varconus}{\ensuremath{\varconu\langs}\xspace}

\newcommand{\varcs}{\ensuremath{\symcs}\xspace}
\newcommand{\varcsh}{\ensuremath{\symcs\langh}\xspace}
\newcommand{\varcsm}{\ensuremath{\symcs\langm}\xspace}

\newcommand{\varexp}{\ensuremath{\symexp}\xspace}
\newcommand{\varexph}{\ensuremath{\varexp\langh}\xspace}
\newcommand{\varexpm}{\ensuremath{\varexp\langm}\xspace}
\newcommand{\varexps}{\ensuremath{\varexp\langs}\xspace}

\newcommand{\varnum}{\ensuremath{\symnum}\xspace}

\newcommand{\varstr}{\ensuremath{\formvar{\symstr}}\xspace}

\newcommand{\varty}{\ensuremath{\symty}\xspace}
\newcommand{\vartyh}{\ensuremath{\varty\langh}}
\newcommand{\vartym}{\ensuremath{\varty\langm}}

\newcommand{\varvalu}{\ensuremath{\symvalu}\xspace}
\newcommand{\varvalum}{\ensuremath{\varvalu\langm}\xspace}
\newcommand{\varvalus}{\ensuremath{\varvalu\langs}\xspace}

\newcommand{\varvalf}{\ensuremath{\symvalf}\xspace}
\newcommand{\varvalfh}{\ensuremath{\varvalf\langh}\xspace}
\newcommand{\varvalfm}{\ensuremath{\varvalf\langm}\xspace}
\newcommand{\varvalfs}{\ensuremath{\varvalf\langs}\xspace}

\newcommand{\varvar}{\ensuremath{\symvar}\xspace}
\newcommand{\varvarh}{\ensuremath{\varvar\langh}\xspace}
\newcommand{\varvarm}{\ensuremath{\varvar\langm}\xspace}
\newcommand{\varvars}{\ensuremath{\varvar\langs}\xspace}

% Expressions

\newcommand{\expadd}[2]{\ensuremath{\formsym{\symadd} \; #1 \; #2}}
\newcommand{\expcons}[2]{\ensuremath{\formsym{\symcons} \; #1 \; #2}}
\newcommand{\experr}[1]{\ensuremath{\formstr{\textbf{Error:}\;#1}}}
\newcommand{\expfabsd}[2]{\ensuremath{\lambda #1 . #2}}
\newcommand{\expfabss}[3]{\ensuremath{\lambda #1 : #2 . #3}}
\newcommand{\expfapp}[2]{\ensuremath{#1 \; #2}}
\newcommand{\expfield}[1]{\ensuremath{\formvar{\symfield} \; #1}}
\newcommand{\exphd}[1]{\ensuremath{\formsym{\symhd} \; #1}}
\newcommand{\exphm}[3]{\ensuremath{\formsym{\symhm} \; #1 \; #2 \; #3}}
\newcommand{\exphs}[2]{\ensuremath{\formsym{\symhs} \; #1 \; #2}}
\newcommand{\expif}[3]{\ensuremath{\formsym{\symif} \; #1 \; #2 \; #3}}
\newcommand{\expmh}[3]{\ensuremath{\formsym{\symmh} \; #1 \; #2 \; #3}}
\newcommand{\expms}[2]{\ensuremath{\formsym{\symms} \; #1 \; #2}}
\newcommand{\expnild}{\ensuremath{\formsym{\symnil}}\xspace}
\newcommand{\expnils}[1]{\ensuremath{\formsym{\symnil} \; #1}}
\newcommand{\expnum}[1]{\ensuremath{\formnum{#1}}}
\newcommand{\expop}[2]{\ensuremath{\formvar{\symop} \; #1 \; #2}}
\newcommand{\exppred}[1]{\ensuremath{\formvar{\sympred} \; #1}}
\newcommand{\exppfun}[1]{\ensuremath{\formsym{\sympfun} \; #1}}
\newcommand{\expplist}[1]{\ensuremath{\formsym{\symplist} \; #1}}
\newcommand{\exppnull}[1]{\ensuremath{\formsym{\sympnull} \; #1}}
\newcommand{\exppnum}[1]{\ensuremath{\formsym{\sympnum} \; #1}}
\newcommand{\expsh}[2]{\ensuremath{\formsym{\symsh} \; #1 \; #2}}
\newcommand{\expsm}[2]{\ensuremath{\formsym{\symsm} \; #1 \; #2}}
\newcommand{\expsub}[2]{\ensuremath{\formsym{\symsub} \; #1 \; #2}}
\newcommand{\expsubst}[3]{\ensuremath{\subst{#1}{#2}{#3}}}
\newcommand{\exptabs}[2]{\ensuremath{\Lambda #1 . #2}}
\newcommand{\exptapp}[2]{\ensuremath{#1 \; \langle #2 \rangle}}
\newcommand{\exptl}[1]{\ensuremath{\formsym{\symtl} \; #1}}
\newcommand{\expwrongd}[1]{\ensuremath{\formsym{\symwrong} \; #1}}
\newcommand{\expwrongs}[2]{\ensuremath{\formsym{\symwrong} \; #1 \; #2}}

% Types

\newcommand{\tylump}{\ensuremath{\formsym{\symlump}}\xspace}
\newcommand{\tynum}{\ensuremath{\formsym{\symnat}}\xspace}
\newcommand{\tyvar}{\ensuremath{\symtyvar}\xspace}
\newcommand{\tyvarh}{\ensuremath{\tyvar\langh}\xspace}
\newcommand{\tyvarm}{\ensuremath{\tyvar\langm}\xspace}
\newcommand{\tylist}[1]{\ensuremath{\synlist{#1}}\xspace}
\newcommand{\tyfun}[2]{\ensuremath{#1 \symfun #2}\xspace}
\newcommand{\tyfor}[2]{\ensuremath{\symfor #1 . #2}\xspace}
\newcommand{\tysubst}[3]{\ensuremath{\subst{#1}{#2}{#3}}}
\newcommand{\tytst}{\ensuremath{\formsym{\symtst}}\xspace}
\newcommand{\tyunbrand}[1]{\ensuremath{\lfloor #1 \rfloor}\xspace}

% Conversion schemes

\newcommand{\cslump}{\ensuremath{\formsym{\symlump}}\xspace}
\newcommand{\csnum}{\ensuremath{\formsym{\symnat}}\xspace}
\newcommand{\csvar}{\ensuremath{\symcsvar}\xspace}
\newcommand{\csvarh}{\ensuremath{\symcsvar\langh}\xspace}
\newcommand{\csvarm}{\ensuremath{\symcsvar\langm}\xspace}
\newcommand{\cslist}[1]{\ensuremath{\synlist{#1}}\xspace}
\newcommand{\csbrand}[2]{\ensuremath{#1 \diamond #2}\xspace}
\newcommand{\csfun}[2]{\ensuremath{#1 \symfun #2}\xspace}
\newcommand{\csfor}[2]{\ensuremath{\symfor #1 . #2}\xspace}
\newcommand{\cssubst}[3]{\ensuremath{\subst{#1}{#2}{#3}}}

% Typing rules

\newcommand{\jud}{\ensuremath{\symjud}\xspace}

\newcommand{\judpair}[2]{#1 \symhasty #2}
\newcommand{\jude}[4]{\ensuremath{#1 #2 \judpair{#3}{#4}}\xspace}
\newcommand{\judeh}[3]{\jude{#1}{\symjudh}{#2}{#3}}
\newcommand{\judem}[3]{\jude{#1}{\symjudm}{#2}{#3}}
\newcommand{\judes}[3]{\jude{#1}{\symjuds}{#2}{#3}}

\newcommand{\judt}[3]{\ensuremath{#1 #2 #3}\xspace}
\newcommand{\judth}[2]{\judt{#1}{\symjudh}{#2}}
\newcommand{\judtm}[2]{\judt{#1}{\symjudm}{#2}}
\newcommand{\judts}[2]{\judt{#1}{\symjuds}{#2}}

\newcommand{\env}{\ensuremath{\symenv}\xspace}
%\newcommand{\envempty}{\ensuremath{\symempty}}
\newcommand{\envexte}[3]{\ensuremath{#1 \symext #2 \symhasty #3}}
\newcommand{\envextt}[2]{\ensuremath{#1 \symext #2}}

% Reduction rules

\newcommand{\redcon}[1]{\ensuremath{\varconm[#1]}}
\newcommand{\redconh}[1]{\ensuremath{\varconm[#1]\langh}}
\newcommand{\redconm}[1]{\ensuremath{\varconm[#1]\langm}}
\newcommand{\redcons}[1]{\ensuremath{\varconm[#1]\langs}}

\newcommand{\red}{\ensuremath{\symred}\xspace}
\newcommand{\redrule}[2]{\ensuremath{#1 \red #2}}
\newcommand{\redruleh}[2]{\ensuremath{\redrule{\redconh{#1}}{\redcon{#2}}}}
\newcommand{\redrulem}[2]{\ensuremath{\redrule{\redconm{#1}}{\redcon{#2}}}}
\newcommand{\redrules}[2]{\ensuremath{\redrule{\redcons{#1}}{\redcon{#2}}}}

\newcommand{\redsp}{\ensuremath{\quad \quad}}

% Formats

\newcommand{\formvar}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\formsym}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\formnum}[1]{\ensuremath{\overline{#1}}}
\newcommand{\formstr}[1]{\ensuremath{\mathrm{#1}}}
\newcommand{\formlang}[1]{\ensuremath{_{\mathit{#1}}}}
\newcommand{\formindex}[2]{\ensuremath{#1^{#2}}}

% Numberings

\newcommand{\first}[1]{\ensuremath{#1}}
\newcommand{\second}[1]{\ensuremath{#1'}}
\newcommand{\third}[1]{\ensuremath{#1''}}
\newcommand{\fourth}[1]{\ensuremath{#1'''}}
\newcommand{\fifth}[1]{\ensuremath{#1''''}}
\newcommand{\ith}[1]{\formindex{#1}{i}}

% Miscellaneous

\newcommand{\str}[1]{\ensuremath{\formstr{``#1"}}}
\newcommand{\subst}[3]{\ensuremath{#1[#2/#3]}}
\newcommand{\synlist}[1]{\ensuremath{\lbrace #1 \rbrace}}
\newcommand{\eq}{\ensuremath{\symlumpeq}\xspace}

% Proof

\newcommand{\proinv}{inversion lemma\xspace}
\newcommand{\prouni}{uniqueness of types lemma\xspace}
\newcommand{\procan}{canonical forms lemma\xspace}
\newcommand{\prouv}{unforced value\xspace}
\newcommand{\prouvs}{\prouv{}s\xspace}

% Errors

\newcommand{\errnum}{\str{Not \; a \; number}\xspace}
\newcommand{\errlist}{\str{Not \; a \; list}\xspace}
\newcommand{\errfun}{\str{Not \; a \; function}\xspace}
\newcommand{\errempty}{\str{Empty \; list}\xspace}
\newcommand{\errtype}{\str{Type \; mismatch}\xspace}
\newcommand{\errbrand}{\str{Brand \; mismatch}\xspace}
\newcommand{\errvalue}{\str{Bad \; value}\xspace}

% Progress

\newcommand{\pscasesone}[3]{If #1 is an \prouv then #2 determines the reduction of #3.}
\newcommand{\pscasestwo}[4]{If #1 is an \prouv then #2 and #3 determine the reduction of #4.}

\newcommand{\pserr}[2]{If #1 \red \emph{\experr{\varstr}} then #2 \red \emph{\experr{\varstr}}.}
\newcommand{\pserrand}[3]{If #1 \red \emph{\experr{\varstr}} and #2 is an \prouv then #3 \red \emph{\experr{\varstr}}.}

\newcommand{\pshyp}[2]{#1 is an \prouv or #1 \red #2 or #1 \red \emph{\experr{\varstr}}}
\newcommand{\pshypby}[2]{\pshyp{#1}{#2} by the induction hypothesis.}

\newcommand{\psother}[2]{#1 and #2 are \prouvs otherwise.}

\newcommand{\pssub}[4]{If #1 \red #2 then #3 \red #4.}
\newcommand{\pssuband}[5]{If #1 \red #2 and #3 is an \prouv then #4 \red #5.}

\newcommand{\psred}[2]{\redrule{#1}{#2}.}
\newcommand{\psredif}[4]{If #1 and #2 are \prouvs then \psred{#1}{#2}}
\newcommand{\psrednote}[3]{\redrule{#1}{#2} $(#3)$.}

\newcommand{\psval}[2]{#1 by lemmas \ref{leminv} and \ref{lemuni} and #2 by lemma \ref{lemcan}.}
\newcommand{\psvalh}[3]{\psval{\judeh{}{#1}{#2}}{#3}}
\newcommand{\psvalm}[3]{\psval{\judem{}{#1}{#2}}{#3}}
\newcommand{\psvaleqh}[3]{\psvalh{#1}{#2}{#1 $=$ #3}}
\newcommand{\psvaleqm}[3]{\psvalm{#1}{#2}{#1 $=$ #3}}
\newcommand{\psvalinh}[3]{\psvalh{#1}{#2}{$#1 \in \lbrace #3 \rbrace$}}
\newcommand{\psvalinm}[3]{\psvalm{#1}{#2}{$#1 \in \lbrace #3 \rbrace$}}
\newcommand{\psvalifone}[2]{If #1 is an \prouv then #2}
\newcommand{\psvaliftwo}[3]{If #1 and #2 are \prouvs then #3}
\newcommand{\psvalifeqh}[3]{\psvalifone{#1}{\psvaleqh{#1}{#2}{#3}}}
\newcommand{\psvalifeqm}[3]{\psvalifone{#1}{\psvaleqm{#1}{#2}{#3}}}
\newcommand{\psvalifinh}[3]{\psvalifone{#1}{\psvalinh{#1}{#2}{#3}}}
\newcommand{\psvalifinm}[3]{\psvalifone{#1}{\psvalinm{#1}{#2}{#3}}}
\newcommand{\psvalcan}[1]{#1 by lemma \ref{lemcan}.}
\newcommand{\psvalcaneq}[2]{\psvalcan{$#1 = #2$}}
\newcommand{\psvalcanin}[2]{\psvalcan{$#1 \in \lbrace #2 \rbrace$}}

% Preservation

\newcommand{\pnpremise}[1]{#1 by the premise and lemma \ref{lemuni}.}
\newcommand{\pntypes}[1]{#1 by lemmas \ref{leminv} and \ref{lemuni}.}
\newcommand{\pnexpsubst}[1]{#1 by lemma \ref{lemexp}.}
\newcommand{\pntysubst}[1]{#1 by lemma \ref{lemtyp}.}

% Temporary

\newcommand{\w}{}
\newcommand{\x}{}
\newcommand{\y}{}
\newcommand{\z}{}