Commit 2026-03-14 09:23 0e3327b2

View on Github →

chore(Order/GameAdd): add elab_as_elim attributes (#33416) This PR does three things:

  • Rename GameAdd.fix to the more illustrative GameAdd.recursion
  • Add elab_as_elim attributes on GameAdd.recursion
  • Deprecate the duplicate GameAdd.induction

Estimated changes

deleted def Prod.GameAdd.fix
deleted theorem Prod.GameAdd.fix_eq
deleted def Sym2.GameAdd.fix
deleted theorem Sym2.GameAdd.fix_eq