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.

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

• toIntId : Nat

@[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.getToIntId : ToIntM Nat

Equations

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

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

Equations

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.