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

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

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

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