Lambda Calculus in Lean

2. L1: Named Terms🔗

import LeanLambda.L0set_option doc.verso true

The second layer restores the syntax that we normally write on paper: variables have names, and lambda abstractions bind names. The semantics of this layer is still given by L0; named terms are translated to de Bruijn terms before we state alpha equivalence and beta reduction.

  1. 2.1. Named Syntax
  2. 2.2. Meaning in L0
  3. 2.3. Named Reduction Rules
  4. 2.4. Reducibility
  5. 2.5. Normal and Neutral Terms
  6. 2.6. Examples