Commit 2024-03-05 18:47 2a65c8db

View on Github →

chore: update unexpanders (#11165) lean4#3375 makes it so that unexpanders do not need to handle overapplication.

Estimated changes

Modified Mathlib/Data/Prod/Basic.lean

added def Prod.delabProdFst

added def Prod.delabProdSnd

deleted def delabProdProjs

deleted def unexpandProdFst

deleted def unexpandProdSnd

Modified Mathlib/Tactic/ProjectionNotation.lean

Modified test/delaborators.lean