Def Mathlib.ProxyType.defaultMkCtorProxyType

Modification history

2023-04-18 03:36
Mathlib/Tactic/ProxyType.lean
feat: `Fintype` deriving handler (#3198) …
Added Mathlib.ProxyType.defaultMkCtorProxyTypeView on Github →