def Lean.Meta.Grind.Arith.isNatType (e : Expr) : Bool

Returns true if e is of the form Nat

def Lean.Meta.Grind.Arith.isIntType (e : Expr) : Bool

Returns true if e is of the form Int

def Lean.Meta.Grind.Arith.isInstAddNat (e : Expr) : Bool

Returns true if e is of the form @instHAdd Nat instAddNat

def Lean.Meta.Grind.Arith.isInstLENat (e : Expr) : Bool

Returns true if e is instLENat

def Lean.Meta.Grind.Arith.isNatAdd? (e : Expr) : Option (Expr × Expr)

Returns some (a, b) if e is of the form

@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) a b

def Lean.Meta.Grind.Arith.isNatAdd (e : Expr) : Bool

Returns true if e is of the form

@HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) _ _

def Lean.Meta.Grind.Arith.isNatNum? (e : Expr) : Option Nat

Returns some k if e @OfNat.ofNat Nat _ (instOfNatNat k)

def Lean.Meta.Grind.Arith.isSupportedType (e : Expr) : Bool

partial def Lean.Meta.Grind.Arith.isRelevantPred (e : Expr) : Bool

def Lean.Meta.Grind.Arith.isArithTerm (e : Expr) : Bool

def Lean.Meta.Grind.Arith.quoteIfArithTerm (e : Expr) : MessageData

Quote e using 「 and 」 if e is an arithmetic term that is being treated as a variable.

partial def Lean.Meta.Grind.Arith.gcdExt (a b : Int) : Int × Int × Int

gcdExt a b returns the triple (g, α, β) such that

• g = gcd a b (with g ≥ 0), and
• g = α * a + β * β.