def Lean.Meta.Grind.Arith.Offset.isCnstr? (e : Expr) : GoalM (Option (Cnstr NodeId))

Equations

• Lean.Meta.Grind.Arith.Offset.isCnstr? e = do let __do_lift ← get pure (Lean.PersistentHashMap.find? __do_lift.arith.offset.cnstrs { expr := e })

def Lean.Meta.Grind.Arith.Offset.assertTrue (c : Cnstr NodeId) (p : Expr) : GoalM Unit

Equations

• Lean.Meta.Grind.Arith.Offset.assertTrue c p = do let __do_lift ← liftM (Lean.Meta.mkOfEqTrue p) Lean.Meta.Grind.Arith.Offset.addEdge c.u c.v c.k __do_lift

def Lean.Meta.Grind.Arith.Offset.assertFalse (c : Cnstr NodeId) (p : Expr) : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.propagateLE : Propagator

Equations

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