Lambda calculus/PL LaTeX macros

lambda-macros.sty

%% Basic Lambda Calculus macros
%% Alex Kavvos, 2021-2023

\ProvidesPackage{lambda-macros}[2024/04/10 lambda-macros]

%% Load in your own work by putting in the same folder as your file and invoking
%%
%%   \usepackage{lambda-macros}
%%

%% We require Jon M. Sterling's delimiters package for nice parentheses.

\RequirePackage{jmsdelim}

%% THE FOLLOWING MACROS REQUIRE THE USE OF **xparse**
%% I HIGHLY RECOMMEND YOU LEARN HOW TO USE IT
%% IT IS ONE OF THE FEW PACKAGES THAT MAKE LaTeX MORE BEARABLE

\RequirePackage{xparse}

%% We also need this to make pretty colours

\RequirePackage{xcolor}

\definecolor{IdiotPurple}{RGB}{102, 51, 102}
\definecolor{FernGreen}{HTML}{467D5E}
\definecolor{ThroneBlue}{RGB}{51, 51, 102}
\definecolor{PermaRed}{RGB}{255, 102, 102}
\definecolor{DogwoodRose}{RGB}{204, 51, 102}
\definecolor{MaizeCrayola}{RGB}{255, 204, 102}
\definecolor{CommandPurple}{RGB}{135, 23, 77}
\definecolor{RegalBlue}{RGB}{3,69,117}
\definecolor{DefinitePurple}{RGB}{77,28,192}

\NewDocumentCommand{\Meta}{m}{{\color{IdiotPurple}{#1}}}
\NewDocumentCommand{\Tm}{m}{{\color{RegalBlue}{#1}}}
\NewDocumentCommand{\Deriv}{m}{{\color{DogwoodRose}{#1}}}

%% Judgements and Induction

\NewDocumentCommand{\IsNat}{m}{#1\ \textsf{nat}}
\NewDocumentCommand{\IsEven}{m}{#1\ \textsf{even}}
\NewDocumentCommand{\IsOdd}{m}{#1\ \textsf{odd}}
\NewDocumentCommand{\IsSum}{mmm}{\textsf{sum}(#1, #2, #3)}
\NewDocumentCommand{\IsList}{m}{#1\ \textsf{list}}
\NewDocumentCommand{\Nil}{}{\textsf{nil}}
\NewDocumentCommand{\Cons}{mm}{\textsf{cons}(#1, #2)}

%% Contexts
\NewDocumentCommand{\EmptyCtx}{}{\cdot}

%% Simple expressions

%% \IsTerm{M}{A}         produces Γ |- Μ : A
%% \IsTerm[\Delta]{M}{A} produces Δ |- M : A
\NewDocumentCommand{\IsTerm}{O{\Gamma}mm}{#1 \vdash \Tm{#2} : #3}

\NewDocumentCommand{\NumT}{}{\textsf{Num}}
\NewDocumentCommand{\StrT}{}{\textsf{Str}}
\NewDocumentCommand{\Num}{m}{\overline{#1}}
\NewDocumentCommand{\Str}{m}{\textsf{str}[#1]}

% Some basic operations
\NewDocumentCommand{\Plus}{mm}{\textsf{plus}(#1; #2)}
\NewDocumentCommand{\Times}{mm}{\textsf{times}(#1; #2)}
\NewDocumentCommand{\ConcatA}{mm}{\textsf{cat}(#1; #2)}
\NewDocumentCommand{\Concat}{mm}{#1 \mathbin{{+}\mspace{-8mu}{+}} #2}
\NewDocumentCommand{\Length}{m}{\textsf{len}(#1)}

\NewDocumentCommand{\Subst}{smmm}{
  \DelimMin{2}
  \IfBooleanTF{#1}{\DelimPrn{\Tm{#2}}}{\Tm{#2}}\Meta{\DelimBrk{\Tm{#3}/\Tm{#4}}}
}

%% STLC

\NewDocumentCommand{\Tuple}{mm}{\DelimGl{#1, #2}}
\NewDocumentCommand{\Proj}{O{1}m}{\pi_{#1}(#2)}
\NewDocumentCommand{\Inl}{m}{\textsf{inl}\DelimPrn{#1}}
\NewDocumentCommand{\Inr}{m}{\textsf{inr}\DelimPrn{#1}}
\NewDocumentCommand{\In}{O{i}m}{\textsf{in}_{#1}\DelimPrn{#2}}
\NewDocumentCommand{\Case}{mmmmm}{\textsf{case}\DelimPrn{#1; #2.\, #3; #4.\, #5}}

\NewDocumentCommand{\UnitT}{}{\mathbf{1}}
\NewDocumentCommand{\UnitV}{}{\langle\rangle}
\NewDocumentCommand{\Void}{}{\mathbf{0}}
\NewDocumentCommand{\Abort}{m}{\textsf{abort}(#1)}

\NewDocumentCommand{\DeclVar}{mm}{#1\mathbin{:}#2}

%% \Lam{x}{e}    produces λx. e
%% \Lam{x}[t]{e} produces λx : t. e
\NewDocumentCommand{\Lam}{mom}{\lambda \IfValueTF{#2}{\DeclVar{#1}{#2}}{#1} .\, #3}

%% \App{e}{e'}  produces e(e')
%% \App*{e}{e'} produces (e)(e')
\NewDocumentCommand{\App}{smm}{\IfBooleanTF{#1}{\DelimPrn{#2}}{#2}\DelimPrn{#3}}

%% Recursion
\NewDocumentCommand{\NatT}{}{\textsf{Nat}}
\NewDocumentCommand{\FName}{m}{\textsf{#1}}
\NewDocumentCommand{\ParTo}{}{\rightharpoonup}
\NewDocumentCommand{\Fix}{mom}{\textsf{fix}\DelimPrn{\IfValueTF{#2}{\DeclVar{#1}{#2}}{#1}.\, #3}}

%% Natural numbers 
\NewDocumentCommand{\Zero}{}{\textsf{zero}}
\NewDocumentCommand{\Succ}{m}{\textsf{succ}(#1)}
\NewDocumentCommand{\Ifz}{mmmm}{\textsf{ifz}(#1; #2; #3.\, #4)}

%% Booleans
\NewDocumentCommand{\BoolT}{}{\textsf{Bool}}
\NewDocumentCommand{\True}{}{\textsf{true}}
\NewDocumentCommand{\False}{}{\textsf{false}}
\NewDocumentCommand{\If}{mmm}{\textsf{if } #1 \textsf{ then } #2 \textsf{ else } #3}

% Let constructs
\NewDocumentCommand{\LetA}{mmm}{\textsf{let}(#1; #2.\, #3)}
\NewDocumentCommand{\Let}{mmm}{\textsf{let}\, #1 \Leftarrow #2\, \textsf{in}\, #3}


%% Operational semantics

\NewDocumentCommand{\IsVal}{m}{\Tm{#1}\ \textsf{val}}
\NewDocumentCommand{\Step}{}{\longmapsto}
\NewDocumentCommand{\StepMany}{}{\mathbin{{\Step}^\ast}}
\NewDocumentCommand{\StepsTo}{mm}{\Tm{#1} \Step \Tm{#2}}
\NewDocumentCommand{\StepsMany}{mm}{\Tm{#1} \StepMany \Tm{#2}}
\NewDocumentCommand{\Eval}{mm}{\Tm{#1} \mathbin{\Downarrow} \Tm{#2}}

%% Contexts

\NewDocumentCommand{\Ctx}{mo}{
  \mathcal{#1}\IfNoValueTF{#2}{\Hole}{\DelimBrk{#2}}
}
\NewDocumentCommand{\Hole}{}{\DelimBrk{-}}

Thank you. For type theory people make their own macros, mostly of the same ilk as the ones found here. (Protip: you can find what other people use by downloading the source code of papers from arXiv). For commutative diagrams it's almost exclusively tikz now (tikz-cd is easier but somewhat more cumbersome for sufficiently complicated diagrams).