1. L0: De Bruijn Terms🔗

import Mathlib.Logic.Relation
import Mathlib.Data.Set.Basic
import LeanLambda.Core

set_option doc.verso true

This first language is the computational core used by the later chapters. Bound variables are represented by de Bruijn indices, while free variables keep their names. This makes substitution and beta reduction executable as ordinary recursive definitions without having to choose fresh names.

1.1. Syntax
1.2. Substitution
1.3. Free Variables
1.4. Beta Reduction
1.5. Examples