structure Lean.Meta.Grind.Arith.Cutsat.ToIntThms : Type

Theorems for operators that have support for i.wrap over i.wrap simplification. Currently only addition and multiplication have wrap cancellation theorems

• c? : Option Expr

  Basic theorem of the form

  toInt a = a' → toInt b = b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')`
  

• c_ww? : Option Expr

  Left-right wrap cancellation theorem of the form

  toInt a = i.wrap a' → toInt b = i.wrap b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
  

• c_wl? : Option Expr

  Left wrap cancellation theorem of the form

  toInt a = i.wrap a' → toInt b = b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
  

• c_wr? : Option Expr

  Right wrap cancellation theorem of the form

  toInt a = a' → toInt b = i.wrap b' → toInt (a ⊞ b) = i.wrap (a' ⊞ b')
  

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntThms : Inhabited ToIntThms

def Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntThms.default : ToIntThms

structure Lean.Meta.Grind.Arith.Cutsat.SymbolicBound : Type

• val : Expr
• ival? : Option Int

def Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicBound.default : SymbolicBound

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicBound : Inhabited SymbolicBound

def Lean.Meta.Grind.Arith.Cutsat.SymbolicBound.isNumeral (b : SymbolicBound) : Bool

inductive Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval : Type

Similar to IntInterval, but with symbolic bounds.

• co (lo hi : SymbolicBound) : SymbolicIntInterval
• ci (lo : SymbolicBound) : SymbolicIntInterval
• io (hi : SymbolicBound) : SymbolicIntInterval
• ii : SymbolicIntInterval

def Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicIntInterval.default : SymbolicIntInterval

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedSymbolicIntInterval : Inhabited SymbolicIntInterval

def Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.isFinite (i : SymbolicIntInterval) : Bool

def Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.lo? (i : SymbolicIntInterval) : Option SymbolicBound

def Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.hi? (i : SymbolicIntInterval) : Option SymbolicBound

def Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.wrap (i : SymbolicIntInterval) (x : Expr) : MetaM Expr

structure Lean.Meta.Grind.Arith.Cutsat.ToIntInfo : Type

• id : Nat
• type : Expr
• u : Level
• toIntInst : Expr
• rangeExpr : Expr
• range : SymbolicIntInterval
• toInt : Expr
• wrap : Expr
• ofWrap0? : Option Expr
• ofEq : Expr
• ofDiseq : Expr
• lowerThm? : Option Expr
• upperThm? : Option Expr
• ofLE? : Option (Option Expr)
• ofNotLE? : Option (Option Expr)
• ofLT? : Option (Option Expr)
• ofNotLT? : Option (Option Expr)
• addThms? : Option ToIntThms
• mulThms? : Option ToIntThms
• subThm? : Option (Option Expr)
• negThm? : Option (Option Expr)
• divThm? : Option (Option Expr)
• modThm? : Option (Option Expr)
• powThm? : Option (Option Expr)
• zeroThm? : Option (Option Expr)
• ofNatThm? : Option (Option Expr)

def Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntInfo.default : ToIntInfo

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntInfo : Inhabited ToIntInfo

structure Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo : Type

For each term e of type α which implements the ToInt α i class, we store its corresponding Int term eToInt, a proof he : toInt e = eToInt, and the type α.

• eToInt : Expr
• α : Expr
• he : Expr