Def Mathlib.Tactic.Order.ToInt.mkFinFun

Modification history

2025-11-16 16:31

Mathlib/Tactic/Order/ToInt.lean

feat(Tactic/Order): translate linear orders to `Int` (#26580) …

Added Mathlib.Tactic.Order.ToInt.mkFinFun View on Github →