source
structure Lean.Meta.Grind.Order.OrderM.Context :
Type

- structId : Nat

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Order.OrderM (α : Type) :
Type
Equations

- Lean.Meta.Grind.Order.OrderM = ReaderT Lean.Meta.Grind.Order.OrderM.Context Lean.Meta.Grind.GoalM

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Order.OrderM.run {α : Type} (structId : Nat) (x : OrderM α) :
GoalM α
Equations

- Lean.Meta.Grind.Order.OrderM.run structId x = x { structId := structId }

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Order.getStructId :
OrderM Nat
Equations

- Lean.Meta.Grind.Order.getStructId = do let __do_lift ← read pure __do_lift.structId

Instances For

source
def Lean.Meta.Grind.Order.getStruct :
OrderM Struct
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Grind.Order.modifyStruct (f : Struct → Struct) :
OrderM Unit
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Grind.Order.getExpr (u : NodeId) :
OrderM Expr
Equations

- Lean.Meta.Grind.Order.getExpr u = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure __do_lift.nodes[u]!

Instances For

source
def Lean.Meta.Grind.Order.getDist? (u v : NodeId) :
OrderM (Option Weight)
Equations

- Lean.Meta.Grind.Order.getDist? u v = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure (Lean.AssocList.find? v __do_lift.targets[u]!)

Instances For

source
def Lean.Meta.Grind.Order.getProof? (u v : NodeId) :
OrderM (Option ProofInfo)
Equations

- Lean.Meta.Grind.Order.getProof? u v = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure (Lean.AssocList.find? v __do_lift.proofs[u]!)

Instances For

source
def Lean.Meta.Grind.Order.getNodeId (e : Expr) :
OrderM NodeId
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Grind.Order.getProof (u v : NodeId) :
OrderM ProofInfo
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Grind.Order.getCnstr? (e : Expr) :
OrderM (Option (Cnstr NodeId))
Equations

- Lean.Meta.Grind.Order.getCnstr? e = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure (Lean.PersistentHashMap.find? __do_lift.cnstrs { expr := e })

Instances For

source
def Lean.Meta.Grind.Order.isRing :
OrderM Bool
Equations

- Lean.Meta.Grind.Order.isRing = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure __do_lift.ringId?.isSome

Instances For

source
def Lean.Meta.Grind.Order.isPartialOrder :
OrderM Bool
Equations

- Lean.Meta.Grind.Order.isPartialOrder = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure __do_lift.isPartialInst?.isSome

Instances For

source
def Lean.Meta.Grind.Order.isLinearPreorder :
OrderM Bool
Equations

- Lean.Meta.Grind.Order.isLinearPreorder = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure __do_lift.isLinearPreInst?.isSome

Instances For

source
def Lean.Meta.Grind.Order.hasLt :
OrderM Bool
Equations

- Lean.Meta.Grind.Order.hasLt = do let __do_lift ← Lean.Meta.Grind.Order.getStruct pure __do_lift.lawfulOrderLTInst?.isSome

Instances For

source
def Lean.Meta.Grind.Order.isInt :
OrderM Bool
Equations

- Lean.Meta.Grind.Order.isInt = do let __do_lift ← Lean.Meta.Grind.Order.getStruct let __do_lift_1 ← liftM Lean.Meta.Grind.getIntExpr pure (Lean.Meta.Grind.isSameExpr __do_lift.type __do_lift_1)

Instances For