Returns true
if e
is of the form Nat
Equations
- Lean.Meta.Grind.Arith.isNatType e = e.isConstOf `Nat
Instances For
Returns true
if e
is of the form Int
Equations
- Lean.Meta.Grind.Arith.isIntType e = e.isConstOf `Int
Instances For
Returns true
if e
is of the form @instHAdd Nat instAddNat
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if e
is instLENat
Equations
- Lean.Meta.Grind.Arith.isInstLENat e = e.isConstOf `instLENat
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Quote e
using 「
and 」
if e
is an arithmetic term that is being treated as a variable.
Equations
Instances For
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
Instances For
Helper monad for collecting decision variables in linarith
and cutsat
- visited : Std.HashSet UInt64
- found : FVarIdSet
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 }
Instances For
@[reducible, inline]
abbrev
Lean.Meta.Grind.Arith.CollectDecVars.CollectDecVarsM.run
(x : CollectDecVarsM Unit)
(decVars : FVarIdSet)
:
Instances For
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 @HMul.hMul 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____