Def Mathlib.Tactic.Order.orderCore

Modification history

2025-10-14 16:26

Mathlib/Tactic/Order.lean

feat(Tactic/Order): frontend for `order` (#27066) …

Added Mathlib.Tactic.Order.orderCore View on Github →