source
def Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.isZero (b : SymbolicBound) :
Bool
Equations

- b.isZero = match b.ival? with | some b => b == 0 | x => false

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.mkIntNegSucc (b : SymbolicBound) :
MetaM Expr

Given a symbolic bound `b`, returns `-b + 1`

Equations

- b.mkIntNegSucc = match b.ival? with | some val => pure (Lean.mkIntLit (-val + 1)) | x => pure (Lean.mkIntAdd (Lean.mkIntNeg b.val) (Lean.mkIntLit 1))

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getToIntId? (type : Expr) :
GoalM (Option Nat)
Equations

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

Instances For

source
structure Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context :
Type

- toIntId : Nat

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Arith.Cutsat.ToIntM (α : Type) :
Type
Equations

- Lean.Meta.Grind.Arith.Cutsat.ToIntM = ReaderT Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context Lean.Meta.Grind.GoalM

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getToIntId :
ToIntM Nat
Equations

- Lean.Meta.Grind.Arith.Cutsat.getToIntId = do let __do_lift ← read pure __do_lift.toIntId

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getInfo :
ToIntM ToIntInfo
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Grind.Arith.Cutsat.modifyInfo (f : ToIntInfo → ToIntInfo) :
ToIntM Unit
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.ToIntM.run? {α : Type} (type : Expr) (x : ToIntM α) :
GoalM (Option α)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.ToIntM.run (type : Expr) (x : ToIntM Unit) :
GoalM Unit
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getOfLE? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getOfNotLE? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getOfLT? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getOfNotLT? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getAddThms :
ToIntM ToIntThms
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getMulThms :
ToIntM ToIntThms
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getSubThm? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getNegThm? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getDivThm? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getModThm? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getPowThm? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getZeroThm? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getOfNatThm? :
ToIntM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.mkToIntVar (e : Expr) :
ToIntM (Expr × Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.getToIntTermType? (e : Expr) :
GoalM (Option Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.isToIntTerm (e : Expr) :
GoalM Bool
Equations

- Lean.Meta.Grind.Arith.Cutsat.isToIntTerm e = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure (Lean.PersistentHashMap.contains __do_lift.toIntTermMap { expr := e })

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.toInt (a : Expr) :
ToIntM (Expr × Expr)
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.toInt? (a type : Expr) :
GoalM (Option (Expr × Expr))
Equations

- Lean.Meta.Grind.Arith.Cutsat.toInt? a type = Lean.Meta.Grind.Arith.Cutsat.ToIntM.run? type (Lean.Meta.Grind.Arith.Cutsat.toInt a)

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.isSupportedType (type : Expr) :
GoalM Bool
Equations

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

Instances For

source
def Lean.Meta.Grind.Arith.Cutsat.assertToIntBounds (e : Expr) (x : Var) :
GoalM Unit

Given `x` whose denotation is `e`, if `e` is of the form `ToInt a`, asserts its lower and upper bounds if available

Equations

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

Instances For