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

Returns true if e is a numeral and has type Nat.

Equations

• One or more equations did not get rendered due to their size.

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

Returns true if e is a nonnegative numeral and has type Int.

Equations

• One or more equations did not get rendered due to their size.

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

Returns true if e is a numeral and has type Int.

Equations

• One or more equations did not get rendered due to their size.

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

Returns true if e is a numeral supported by cutsat.

Equations

• Lean.Meta.Grind.Arith.isNum e = (Lean.Meta.Grind.Arith.isNatNum e || Lean.Meta.Grind.Arith.isIntNum e)

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

Returns true if e is of the form Nat

Equations

• Lean.Meta.Grind.Arith.isNatType e = e.isConstOf `Nat

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

Returns true if e is of the form Int

Equations

• Lean.Meta.Grind.Arith.isIntType e = e.isConstOf `Int

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Returns true if e is instLENat

Equations

• Lean.Meta.Grind.Arith.isInstLENat e = e.isConstOf `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

Equations

• One or more equations did not get rendered due to their size.

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) _ _

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Grind.Arith.isSupportedType e = (Lean.Meta.Grind.Arith.isNatType e || Lean.Meta.Grind.Arith.isIntType e)

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lean.Meta.Grind.Arith.quoteIfArithTerm e = if Lean.Meta.Grind.Arith.isArithTerm e = true then Lean.aquote (Lean.MessageData.ofExpr e) else Lean.MessageData.ofExpr e

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 + β * b.

partial def Lean.Meta.Grind.Arith.shrink (a : PArray Rat) (sz : Nat) : PArray Rat

def Lean.Meta.Grind.Arith.resize (a : PArray Rat) (sz : Nat) : PArray Rat

Equations

• Lean.Meta.Grind.Arith.resize a sz = if a.size > sz then Lean.Meta.Grind.Arith.shrink a sz else Lean.Meta.Grind.Arith.resize.go✝ sz a

Helper monad for collecting decision variables in linarith and cutsat

structure Lean.Meta.Grind.Arith.CollectDecVars.State : Type

• visited : Std.HashSet UInt64
• found : FVarIdSet

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CollectDecVars.CollectDecVarsM (α : Type) : Type

Equations

• Lean.Meta.Grind.Arith.CollectDecVarsM = ReaderT Lean.FVarIdSet (StateM Lean.Meta.Grind.Arith.CollectDecVars.State)

def Lean.Meta.Grind.Arith.CollectDecVars.alreadyVisited {α : Type u_1} (c : α) : CollectDecVarsM Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.CollectDecVars.markAsFound (fvarId : FVarId) : CollectDecVarsM Unit

Equations

• Lean.Meta.Grind.Arith.CollectDecVars.markAsFound fvarId = modify fun (s : Lean.Meta.Grind.Arith.CollectDecVars.State) => { visited := s.visited, found := s.found.insert fvarId }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CollectDecVars.CollectDecVarsM.run (x : CollectDecVarsM Unit) (decVars : FVarIdSet) : FVarIdSet

Equations

• x.run decVars = match StateT.run (x decVars) { } with | (fst, s) => s.found

def Lean.Meta.Grind.Arith.getIntModuleVirtualParent : Expr

Return auxiliary expression used as "virtual" parent when internalizing auxiliary expressions created by toIntModuleExpr. The function toIntModuleExpr converts a CommRing polynomial into a IntModule expression. We don't want this auxiliary expression to be internalized by the CommRing module since it uses a nonstandard encoding with @HSMul.hSMul Int α α, a virtual One.one constant, etc.

Equations

• Lean.Meta.Grind.Arith.getIntModuleVirtualParent = Lean.mkConst `_private.Lean.Meta.Tactic.Grind.Arith.Util.0.Lean.Meta.Grind.Arith.____intModuleMarker____

def Lean.Meta.Grind.Arith.isIntModuleVirtualParent (parent? : Option Expr) : Bool

Equations

• Lean.Meta.Grind.Arith.isIntModuleVirtualParent none = false
• Lean.Meta.Grind.Arith.isIntModuleVirtualParent (some parent) = (parent == Lean.Meta.Grind.Arith.getIntModuleVirtualParent)

@[specialize #[]]

def Lean.Meta.Grind.Arith.split {α : Type u_1} (cs : PArray α) (getCoeff : α → Int) : PArray α × Array (Int × α)

Equations

• One or more equations did not get rendered due to their size.