def Lean.Meta.Grind.Order.getStructId? (type : Expr) : GoalM (Option Nat)

Returns the order structure id for type, if it is at least a preorder. The classification is done and cached by Sym.Arith.classifyOrder? for the whole run; this function only applies the order configuration flag.

Equations

• Lean.Meta.Grind.Order.getStructId? type = do let __do_lift ← liftM Lean.Meta.Grind.getConfig if __do_lift.order = true then liftM (Lean.Meta.Sym.Arith.classifyOrder? type) else pure none