def Lean.Meta.Grind.Arith.Cutsat.getToIntInfo? (type : Expr) : GoalM (Option ToIntInfo)

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.getToIntInfo?.toIntInterval? (type rangeExpr : Expr) : GoalM (Option Grind.IntInterval)

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.getToIntInfo?.go? (type : Expr) : GoalM (Option ToIntInfo)

Equations

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

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

• info : ToIntInfo

@[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

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.getInfo = do let __do_lift ← read pure __do_lift.info

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.

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.ToIntM.run type x = do let __discr ← Lean.Meta.Grind.Arith.Cutsat.getToIntInfo? type match __discr with | some info => x { info := info } | x => pure ()

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.

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.

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

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.

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)

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

Equations

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

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.