Commit 2023-10-13 21:18 01666422

View on Github →

feat: long overdue delaborators (#7633) This brings to Mathlib assorted delaborators written by @kmill for various projects including Mathematics in Lean. They mostly fix regressions compared to Lean 3.

Estimated changes

Modified Mathlib/Data/Prod/Basic.lean

added def delabProdProjs

added def unexpandProdFst

added def unexpandProdSnd

Modified Mathlib/Data/Set/Lattice.lean

added def Set.iUnion_delab

added def Set.sInter_delab

Modified Mathlib/Order/CompleteLattice.lean

added def iInf_delab

added def iSup_delab

Modified Mathlib/Util/PiNotation.lean

added def PiNotation.delabPi'

added def exists_delab

Created test/delaborators.lean

Modified test/propose.lean