Repository navigation

feat(untyped): standardization theorem for the lambda calculus - #679

Merged

chenson2018 merged 17 commits into

leanprover:mainfrom

m-ow:standardization-theorem

Jul 9, 2026

Merged

feat(untyped): standardization theorem for the lambda calculus#679
chenson2018 merged 17 commits into
leanprover:mainfrom
m-ow:standardization-theorem

Commits on Jul 7, 2026
- add basic properties
  m-ow
  committed
  70543ce
- add standardization theorem
  m-ow
  committed
  93dfbbb
- fix notation
  m-ow
  committed
  58eca13
Commits on Jul 8, 2026
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  668a47f
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  2b89df8
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  a9ced4f
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  94f3477
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  d21d9da
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  a2a5b28
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  7b43362
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  1399c5f
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  authored
  582d715
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
  
  m-ow
  and
  chenson2018
  authored
  ee31d1d
- refactor proofs per review feedback
  m-ow
  committed
  60c2d5b
- add Trans instances for standard reduction
  m-ow
  committed
  31c1f37
Commits on Jul 9, 2026
- split out branches of grind proofs
  chenson2018
  committed
  624ddbd
- misc namespace golf
  chenson2018
  committed
  c188914

Commits

Commits on Jul 7, 2026

Commits on Jul 8, 2026

Commits on Jul 9, 2026