Def Foo

Modification history

2026-10-24 08:53

MathlibTest/Delab/PPWithUniv.lean

fix: setting `pp.mdata` to true breaks `@[pp_with_univ]` (#43981) …

Added Foo View on Github →

2026-01-15 16:12

MathlibTest/UnusedInstancesInType/Fintype.lean

feat: `unusedFintypeInType` linter (#31794) …

Added Foo View on Github →

2025-11-25 19:25

MathlibTest/UnusedInstancesInType.lean

feat(Linter): port unused `Decidable*` instance hypothesis linter (#31142) …

Added Foo View on Github →