Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat

Equations
    Instances For

      Given e of the form lhs ≤ rhs where lhs and rhs have type Nat, returns (lhs, rhs) where lhs and rhs are Int.OfNat.Expr.

      Equations
        Instances For
          Equations
            Instances For

              Given e of type Int, tries to compute a : Int.OfNat.Expr s.t. a.denoteAsInt ctx is e

              If e is of the form a.denoteAsInt ctx for some a and ctx, assert that e is nonnegative.

              Equations
                Instances For

                  Given x whose denotation is e, if e is of the form NatCast.natCast a, asserts that it is nonnegative.

                  Equations
                    Instances For