Lambda Calculus in Lean

3. L2: Simple Types🔗

import LeanLambda.L1 import LeanLambda.Tacticsset_option doc.verso true

This layer keeps the named terms from L1 and adds simple types and typing judgments. The terms do not change; only the propositions we prove about them become typed.

  1. 3.1. Type Expressions
  2. 3.2. Typing Contexts
  3. 3.3. Typing Judgment
  4. 3.4. Metatheory