Lambda Calculus in TeX

lambda.tex

\documentclass[a4paper]{article}

\usepackage[T1]{fontenc}
\usepackage{geometry}
\usepackage{fancyvrb}
\fvset{tabsize=2}

\title{Lambda Calculus in \TeX}
\author{Camil Staps}

\makeatletter

% TeX for loop
\def\for#1=#2:#3{\ifor{#1}{#3}#2}
\def\ifor#1#2#3{%
	\xdef#1{#3}%
	#2%
	\kernel@ifnextchar,{\iforcomma{#1}{#2}}\relax}
\def\iforcomma#1#2,{\ifor{#1}{#2}}

% IKS
\def\i#1{\csname#1\endcsname}
\def\k#1#2{#1}
\def\s#1#2#3{\csname#1\endcsname{#3}{\csname#2\endcsname{#3}}}

% Booleans
\def\True#1#2{#1}
\def\False#1#2{#2}
\def\And#1#2{\csname#1\endcsname{#2}{#1}}
\def\Ior#1#2{\csname#1\endcsname{#1}{#2}}
\def\Not#1{\csname#1\endcsname{False}{True}}
\def\Xor#1#2{\And{\Ior{#1}{#2}}{\Not{\And{#1}{#2}}}}

% Numbers (Barendregt numerals)
\def\Zero#1{}
\def\Succ#1#2{\csname#2\endcsname{False}{#1}}

% Printing numbers
\def\@print#1#2{#2{@print}{\global\advance\count255 by 1}}%
\def\print#1{%
	\count255=0
	#1{@print}%
	\number\count255}

\makeatother
\begin{document}

\maketitle
\thispagestyle{empty}

\section*{Booleans}
\VerbatimInput[firstline=27,lastline=32]{lambda.tex}
\VerbatimInput[firstline=55,lastline=60]{lambda.tex}

\begin{center}
\begin{tabular}{llllll}
	$p$ & $q$ & $\lnot p$ & $p \land q$ & $p \lor q$ & $p \oplus q$ \\\hline
	\for\p={False},{True}:{%
		\for\q={False},{True}:{%
			\p & \q & \Not{\p} & \And{\p}{\q} & \Ior{\p}{\q} & \Xor{\p}{\q}\\}}
\end{tabular}
\end{center}

\section*{Barendregt numerals}
\VerbatimInput[firstline=35,lastline=36]{lambda.tex}
\VerbatimInput[firstline=39,lastline=43]{lambda.tex}
\VerbatimInput[firstline=70,lastline=70]{lambda.tex}

\begin{center}
\print{\Succ{\Succ{\Succ{\Zero}}}}
\end{center}

\end{document}