type-theory-macros

type-theory-macros.sty

%% Basic Type Theory macros
%% Alex Kavvos, 2024-
%% with thanks to Daniel Gratzer

\ProvidesPackage{lambda-macros}[2024/02/20 type-theory-macros]

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

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

\RequirePackage{jmsdelim}

%% We also require the macros for basic lambda calculus

\RequirePackage{lambda-macros}

%% 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}

\NewDocumentCommand{\DSum}{mmm}{\DelimMin{1} \DelimPrn{\DeclVar{#1}{#2}} \times #3}
\NewDocumentCommand{\DProd}{mmm}{\DelimMin{1} \DelimPrn{\DeclVar{#1}{#2}} \to #3}

\NewDocumentCommand{\IsCtx}{m}{#1\ \mathsf{ctx}}
\NewDocumentCommand{\IsTy}{O{\Gamma}m}{#1 \vdash #2}
\NewDocumentCommand{\IsTm}{O{\Gamma}mm}{#1 \vdash #2 \colon #3}

\NewDocumentCommand{\EmpCx}{}{\cdot}
\NewDocumentCommand{\ECx}{mmm}{#1, \DeclVar{#2}{#3}}