Repository navigation

feat: de Bruijn Syntax for Untyped Lambda Calculus and a proof of Church-Rosser with Parallel Reduction - #475

Open

zayn7lie wants to merge 35 commits into

leanprover:mainfrom

zayn7lie:main

Open

feat: de Bruijn Syntax for Untyped Lambda Calculus and a proof of Church-Rosser with Parallel Reduction#475
zayn7lie wants to merge 35 commits into
leanprover:mainfrom
zayn7lie:main

Commits on Oct 17, 2026
- feat: Church–Rosser theorem (Q1308502) for ULC (de Bruijn)
  zayn7lie
  committed
  55aac0c
- upd: change dir
  zayn7lie
  committed
  bcfca97
- upd: localize from to
  zayn7lie
  committed
  f2c0926
- upd: eliminate for de bruijn syntax and explicit all and
  zayn7lie
  committed
  7611b04
- upd: eliminate for diamond and Confluent definition
  zayn7lie
  committed
  e600c64
- upd: generalize decrement for consistency
  zayn7lie
  committed
  e07b8c3
- upd: instantiate with
  zayn7lie
  committed
  70967bb
- upd: newline between theorems
  zayn7lie
  committed
  dd4dd39
- upd: clean up `ConfluentReduction.lean` to `Cslib.Foundations.Data.Relation`, and add `rtc_eq_of_sandwich`
  zayn7lie
  committed
  89bb8e5
- upd: clean up `ConfluentReduction.lean` to `Cslib.Foundations.Data.Relation`, and add `rtc_eq_of_sandwich`
  zayn7lie
  committed
  6c5d50e
- upd: clarification for consistency of decre
  zayn7lie
  committed
  fbc1567
- upd: `reduction_sys` for generating notations for reductions and the multi-step closure
  zayn7lie
  committed
  367fece
- fix: notation typeclass for substitution
  zayn7lie
  committed
  e0d47e8
- fix: sandwich
  zayn7lie
  committed
  2bb6b42
- fix: par_subst - lt_trichotomy
  zayn7lie
  committed
  1296ebc
- fix: syntax - disambiuity
  zayn7lie
  committed
  93efa90
- upd: syntax - sub - specify type
  zayn7lie
  committed
  007a476
- upd: syntax - Term - docstring
  zayn7lie
  committed
  4b9e5dc
- upd: xyntax - incre_rfl - proof
  zayn7lie
  committed
  a65a9b9
- fix: namespace
  zayn7lie
  committed
  75817ce
- upd: open term redundent
  zayn7lie
  committed
  51e099e
- upd: \@\[expose\] public section
  zayn7lie
  committed
  89e157a
- upd: betareduction - proof simp
  zayn7lie
  committed
  afac21b
- upd: typo
  zayn7lie
  committed
  3ea56a2
- upd: betareduction
  zayn7lie
  committed
  88f98b2
- fix: debruijn - where
  zayn7lie
  committed
  f94c25e
- upd: debruijn def - dosctring
  zayn7lie
  committed
  d9720d1
- upd: Nat.assoc update
  zayn7lie
  committed
  89c9887
- upd: Relation after split, sandwich_to_eq
  zayn7lie
  committed
  89ca52c
- upd: final resolve Conflicts
  zayn7lie
  committed
  e8dec0d
- fix: ParStar definition
  zayn7lie
  committed
  492b21b
- fix: remove whitespace
  zayn7lie
  committed
  194d9c3
- upd: subst sandwich with reflTransGen_mono_closed
  zayn7lie
  committed
  a6d4f67
- upd: DeBruijnSyntax - `if_neg` has been deprecated: Use `ite_eq_right` instead
  zayn7lie
  committed
  c16b3af
- fix: has been deprecated: Use `Relation.Diamond.to_confluent` instead
  zayn7lie
  committed
  cd9bd6b

Commits

Commits on Oct 17, 2026