def Lean.Meta.Grind.Arith.Cutsat.mkVar (expr : Expr) : GoalM Var

Creates a new variable in the cutsat module.

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.isInt (e : Expr) : GoalM Bool

Equations

• Lean.Meta.Grind.Arith.Cutsat.isInt e = do let __do_lift ← liftM (Lean.Meta.inferType e) liftM (Lean.Meta.isDefEq __do_lift (Lean.mkConst `Int))

def Lean.Meta.Grind.Arith.Cutsat.isAdd? (e : Expr) (report : Bool := true) : GoalM (Option (Expr × Expr))

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.isAdd (e : Expr) : GoalM Bool

Equations

• Lean.Meta.Grind.Arith.Cutsat.isAdd e = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.isAdd? e false pure __do_lift.isSome

def Lean.Meta.Grind.Arith.Cutsat.isMul? (e : Expr) (report : Bool := true) : GoalM (Option (Int × Expr))

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.isMul (e : Expr) : GoalM Bool

Equations

• Lean.Meta.Grind.Arith.Cutsat.isMul e = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.isMul? e false pure __do_lift.isSome

def Lean.Meta.Grind.Arith.Cutsat.addMonomial (e : Expr) (p : Poly) : GoalM Poly

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.toPoly (e : Expr) : GoalM Poly

Equations

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

partial def Lean.Meta.Grind.Arith.Cutsat.toPoly.go (e : Expr) (p : Poly) : GoalM Poly