Repository navigation

feat(untyped): the Leftmost Reduction Theorem - #700

Merged

chenson2018 merged 24 commits into

leanprover:mainfrom

m-ow:leftmost-reduction

Aug 9, 2026

Merged

feat(untyped): the Leftmost Reduction Theorem#700
chenson2018 merged 24 commits into
leanprover:mainfrom
m-ow:leftmost-reduction

Commits on Jul 14, 2026
- add reference
  m-ow
  committed
  3ee390c
- update Cslib
  m-ow
  committed
  c3227c0
- add leftmost reduction definitions
  m-ow
  committed
  a160398
- add redex counting and normal form lemmas
  m-ow
  committed
  373bcf2
- add basic properties of BetaAt
  m-ow
  committed
  da59187
- add lemmas for leftmost reduction
  m-ow
  committed
  b7705d6
- add leftmost reduction theorem
  m-ow
  committed
  8b37079
- replace aesop with grind
  m-ow
  committed
  7dbff90
- use dot notation
  m-ow
  committed
  d398e52
- simplify BetaAt.rename proof
  m-ow
  committed
  705d44b
- rename NormalForm to BetaNormal
  m-ow
  committed
  d1c4e4e
- add standard sequences and equivalence with Standard
  m-ow
  committed
  9da46d9
- add grind annotation to IsAbs
  m-ow
  committed
  d8b2581
- Update Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
  
  m-ow
  and
  chenson2018
  committed
  00a6478
- specialize countRedexes_openRec_fvar
  m-ow
  committed
  711c9c8
- reorder BetaAt
  m-ow
  committed
  8e91cf8
- move IsAbs next to Value
  m-ow
  committed
  56f8941
- replace appNoAbs/appAbs pairs with appL/appR
  m-ow
  committed
  58869ce
- refactor StandardSeq to follow ReflTransGen
  m-ow
  committed
  6f9e7a1
- group theorems
  m-ow
  committed
  3435855
- split BetaAt into a separate module
  m-ow
  committed
  b8f68f7
- add grind annotations for redex counting
  m-ow
  committed
  61090e1
Commits on Jul 20, 2026
- follow Copes: single-index StandardSeq
  m-ow
  committed
  585ac71
Commits on Aug 9, 2026
- Merge remote-tracking branch 'origin/main' into leftmost-reduction
  chenson2018
  committed
  974aed5

Commits

Commits on Jul 14, 2026

Commits on Jul 20, 2026

Commits on Aug 9, 2026