Repository navigation

refactor(Locallynameless): abbrev multiApp = List.foldl app - #710

Open

lengyijun wants to merge 7 commits into

leanprover:mainfrom

awesome-lambda-calculus:multiapp

Open

refactor(Locallynameless): abbrev multiApp = List.foldl app#710
lengyijun wants to merge 7 commits into
leanprover:mainfrom
awesome-lambda-calculus:multiapp

Commits on Oct 17, 2026
- refactor(Locallynameless): abbrev multiApp = `List.foldl app`
  lengyijun
  committed
  c906723
- feat: `ListFullBeta` context lemmas
  lengyijun
  committed
  85df5fd
- Add `multiApp` congruence lemmas for union reductions
  lengyijun
  committed
  1482228
- format
  lengyijun
  committed
  4768f4d
- multiApp_lc: 32.825737s => 0.411336s
  lengyijun
  committed
  a5f06ae
- concat => append
  lengyijun
  committed
  a0209a3
- simp only [List.foldl_concat]
  lengyijun
  committed
  1c4ed24