Def Mathlib.Tactic.toFunImpl

Modification history

2026-03-16 05:13

Mathlib/Tactic/ToFun.lean

feat(translate): support `to_additive (attr := to_fun)` (#36305) …

Added Mathlib.Tactic.toFunImpl View on Github →