agda/notes/papers/implicit/macros.tex

\newlength\TODOWidth

% Administrative
\newcommand\TODO[1]{\footnote{TODO: {#1}}}
% \newcommand\TODO[1]{
% \par
% \vspace{1mm}
% \fbox{
% \setlength\TODOWidth{\textwidth}
% \addtolength\TODOWidth{-60pt}
% \begin{tabular}{p{\TODOWidth}}
%     TODO: #1
% \end{tabular}}
% }
% \newcommand\TODO[1]{\par{
%     \setbox0=\vbox{{\small \parbox{35mm}{#1}}} %{\parbox{3.5cm}{{\small #1}}}
%     \hskip-50mm\copy0
%     \vskip-\ht0
%     \vskip-2mm
% }\par
% }

\newcommand\Core{{\sf\bf MLF}}

% Misc
\renewcommand\Or{~~|~~}
\newcommand\C{\mathcal C}
\newcommand\Pair[1]{\langle#1\rangle}

% Syntax
\newcommand\SET{\mathsf{Set}}
\newcommand\EL{\mathsf{El}\,}
\newcommand\unify{\mathsf{unify}}
\newcommand\inscope{\mathsf{InScope}}
\newcommand\PI[2]{(#1:#2)\to{}}
\newcommand\LAM[1]{\lambda #1.{}}

\newcommand\Subst[3]{ {#1} [ {#3} / {#2} ] }
\newcommand\SubstD[2]{{#1} [ {#2} ] }

% Judgement forms

% Core
\newcommand\IsSigCS[1]{{} \vdash_{#1}}
\newcommand\IsCtxCS[2]{{#2} \vdash_{#1}}
\newcommand\IsTypeCS[3]{{#2} \vdash_{#1}#3 ~ \mathbf{type}}
\newcommand\HasTypeCS[4]{{#2} \vdash_{#1} {#3} : {#4}}
\newcommand\CheckTypeCS[4]{{#2} \vdash_{#1}#3\uparrow#4}
\newcommand\InferTypeCS[4]{{#2} \vdash_{#1}#3\downarrow#4}
\newcommand\EqualTypeCS[4]{{#2} \vdash_{#1}#3=#4}
\newcommand\EqualCS[5]{{#2} \vdash_{#1}#3=#4:#5}

\newcommand\IsCtxC[1]{\IsCtxCS{}{#1}}
\newcommand\IsTypeC[2]{\IsTypeCS{}{#1}{#2}}
\newcommand\HasTypeC[3]{\HasTypeCS{}{#1}{#2}{#3}}
\newcommand\CheckTypeC[3]{\CheckTypeCS{}{#1}{#2}{#3}}
\newcommand\InferTypeC[3]{\InferTypeCS{}{#1}{#2}{#3}}
\newcommand\EqualTypeC[3]{\EqualTypeCS{}{#1}{#2}{#3}}
\newcommand\EqualC[4]{\EqualCS{}{#1}{#2}{#3}{#4}}

% With metas
\newcommand\Cs{\mathcal{C}}

\newcommand\Ext[1]{{#1},\,{}}

\newcommand\ExplicitJudgement[3]{
    \langle {#1} \rangle ~ {#2} \Longrightarrow \langle {#3} \rangle
}

\newcommand\MetaDecl[2]{{#1} : {#2}}

\newcommand\IMetaDecl[3]{{#1} : {#2} = {#3}}

\newcommand\ConstDecl[4]{{#1} : {#2} = {#3} ~\mathbf{when}~ {#4}}

\newcommand\AddMeta[2]{\mathsf{AddMeta}({#1} : {#2})}
\newcommand\AddConst[4]{\mathsf{AddConst}({#1} : {#2} = {#3}~\mathbf{when}~{#4})}
\newcommand\InstMeta[2]{{#1} := {#2}}
\newcommand\LookupMeta[2]{\mathsf{LookupMeta}({#1} = {#2})}
\newcommand\LookupConst[2]{\mathsf{LookupConst}({#1} = {#2})}
\newcommand\LookupType[2]{\mathsf{Lookup}({#1} : {#2})}
\newcommand\InScope[2]{\mathsf{InScope}_{#1}({#2})}
\newcommand\Simplify{\mathsf{SolveConstraints}}
\newcommand\WithSig[1]{\langle {#1} \rangle \,}
\newcommand\UpdateGuard[2]{\mathsf{UpdateGuard}( {#1},\, {#2} )}
\newcommand\LookupClause[3]{\mathsf{Lookup}({#1}~{#2} = {#3})}
\newcommand\Match[3]{\mathsf{Match}({#1}\,{#2} = {#3})}
\newcommand\Guarded[1]{\mathsf{Guarded}({#1})}
\newcommand\Uninstantiated[1]{\mathsf{Uninstantiated}({#1})}
\newcommand\Blocked[1]{\mathsf{Blocked}({#1})}
\newcommand\Inline[2]{{#1} \to_{\mathit{inline}} {#2}}

\newcommand\IsTypeCtx[3]{{#1} \vdash {#2} ~ \mathbf{type} ~ \leadsto {#3}}
\newcommand\CheckTypeCtx[4]{{#1} \vdash {#2} \uparrow {#3} \leadsto {#4}}
\newcommand\InferTypeCtx[4]{{#1} \vdash {#2} \downarrow {#3} \leadsto {#4}}
\newcommand\EqualTypeCtx[4]{{#1} \vdash {#2} = {#3} \leadsto {#4}}
\newcommand\EqualCtx[5]{{#1} \vdash {#2} = {#3} : {#4} \leadsto {#5}}
\newcommand\EqualWhnfCtx[5]{{#1} \vdash {#2} \doteq {#3} : {#4} \leadsto {#5}}
% \newcommand\EqualWhnfCtx[5]{{#1} \vdash {#2} \mathrel{\stackrel{\mathit{whnf}}=} {#3} : {#4} \leadsto {#5}}

\newcommand\TypeConstrCtx[3]{\EqualTypeC {#1} {#2} {#3}}
\newcommand\TermConstrCtx[4]{\EqualC {#1} {#2} {#3} {#4}}
\newcommand\TypeConstr[2]{\TypeConstrCtx \Gamma {#1} {#2}}
\newcommand\TermConstr[3]{\TermConstrCtx \Gamma {#1} {#2} {#3}}
\newcommand\ValidConstr[2]{\vdash_{#1} {#2} ~ \mathbf{ok}}
\newcommand\TrueConstr[2]{\vdash_{#1} {#2} ~ \mathbf{true}}

\newcommand\IsType[2]{\IsTypeCtx \Gamma {#1} {#2}}
\newcommand\CheckType[3]{\CheckTypeCtx \Gamma {#1} {#2} {#3}}
\newcommand\InferType[3]{\InferTypeCtx \Gamma {#1} {#2} {#3}}
\newcommand\EqualType[3]{\EqualTypeCtx \Gamma {#1} {#2} {#3}}
\newcommand\Equal[4]{\EqualCtx \Gamma {#1} {#2} {#3} {#4}}
\newcommand\EqualWhnf[4]{\EqualWhnfCtx \Gamma {#1} {#2} {#3} {#4}}
\newcommand\CheckConstr[2]{{#1} \leadsto {#2}}

\newcommand\whnf[2]{{#1} \to_{\mathit{whnf}} {#2}}
\newcommand\Normalise[2]{{#1} \to_{\mathit{nf}} {#2}}

\newcommand\FV[1]{\mathsf{FV}({#1})}
\newcommand\AppSub[2]{{#2}{#1}}

\newcommand\CombinedSig[3]{\mathsf{Combine}({#1},{#2},{#3})}
\newcommand\CoreSig[1]{\left|{#1}\right|}
\newcommand\Implements[2]{{#2} \propto {#1}}

\newcommand\Extends[2]{{#1} ~ \mathit{extends} ~ {#2}}

\newcommand\Rules[2]{
\par~\par
{\setlength\parindent{0mm}
    {\em #1}{\small
    \[\begin{array}{c}
	#2
    \end{array}\]
    }
}}

\newcommand\URules[1]{
{\small\[\begin{array}{c}
    #1
\end{array}\]
}}

\newcommand\Rule[2]{\frac{\displaystyle{#2}}{\displaystyle\begin{array}{l}#1\end{array}}}