Documentation

Lean.Meta.Tactic.Simp.Arith.Int.Simp

source
def Int.Internal.Linear.Poly.gcdAll :
Poly → Nat
Instances For
    source
    def Int.Internal.Linear.Poly.gcdCoeffs' :
    Poly → Nat
    Instances For
      source
      def Lean.Meta.Simp.Arith.Int.simpEq? (e : Expr) :
      MetaM (Option (Expr × Expr))
      Instances For
        source
        def Lean.Meta.Simp.Arith.Int.simpLe? (e : Expr) (checkIfModified : Bool) :
        MetaM (Option (Expr × Expr))
        Instances For
          source
          def Lean.Meta.Simp.Arith.Int.simpRel? (e : Expr) :
          MetaM (Option (Expr × Expr))
          Instances For
            source
            def Lean.Meta.Simp.Arith.Int.simpDvd? (e : Expr) :
            MetaM (Option (Expr × Expr))
            Instances For
              source
              def Lean.Meta.Simp.Arith.Int.simpExpr? (lhs : Expr) :
              MetaM (Option (Expr × Expr))
              Instances For