Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr

source
def Lean.Meta.Grind.Arith.Linear.IneqCnstr.assert (c : IneqCnstr) :
LinearM Unit
Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.Linear.propagateIneq (e : Expr) (eqTrue : Bool) :
      GoalM Unit
      Equations
        Instances For