Documentation

Lean.Meta.Tactic.Simp.Arith.Nat.Simp

source
def Lean.Meta.Simp.Arith.Nat.simpCnstrPos? (e : Expr) :
MetaM (Option (Expr × Expr))
Equations
    Instances For
      source
      def Lean.Meta.Simp.Arith.Nat.simpCnstr? (e : Expr) :
      MetaM (Option (Expr × Expr))
      Equations
        Instances For
          source
          def Lean.Meta.Simp.Arith.Nat.simpExpr? (input : Expr) :
          MetaM (Option (Expr × Expr))
          Equations
            Instances For