Functional Programming in Lean

Dakota Bryan

Thursday, October 2, 2025

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferlab}[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\inferright}[3]{ \let\and\qquad \displaystyle \frac{#2}{#3}\TirName{#1} } \newcommand{\inferrule}[3][]{\inferlab{#1}{#2}{#3}} \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

Meeting 13 - Functional Programming in Lean

What questions do you have? What questions does your neighbor have?

Links

Full Code with some commented explanations

In-Class Code

Lean Installation

Install through the VS Code extension

JavaScripty

Grammar

Syntax and Semantics

Big Step Semantics

Induction

Small Step Semantics

Meta Theory

Other Judgments

evalExpr

\[ \fbox{$\rho \vdash e \Downarrow\rho'$} \]

valToBool i.e. “truthy”

\[ \fbox{$v\Downarrow_bb$} \]

\(\inferrule[EvalBool]{ \phantom{\Downarrow} }{ b\Downarrow_bb }\)

\(\inferrule[EvalNumZero]{ n= 0 }{ n\Downarrow_b\mathbf{false} }\)

\(\inferrule[EvalNumNotZero]{ n\neq 0 }{ n\Downarrow_b\mathbf{true} }\)

valToNum \[ \fbox{$v\Downarrow_nn$} \]

evalUop \[ \fbox{$\mathit{uop}, v_1 \hookrightarrow v$} \]

\(\inferrule[EvalLogicalNegate]{ v_1 \Downarrow_bb }{ \texttt{!}, v_1 \hookrightarrow \neg b }\)

\(\inferrule[EvalNumericalNegate]{ v_1 \Downarrow_nn }{ \texttt{-}, v_1 \hookrightarrow - n }\)

evalBop \[ \fbox{$\mathit{bop}, v_1, v_2 \hookrightarrow v$} \]