def Lean.Meta.Grind.Arith.Cutsat.mkForeignVar (e : Expr) (t : ForeignType) : GoalM Var

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.foreignTerm? (e : Expr) : GoalM (Option ForeignType)

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.hasForeignVar e = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure (Lean.PersistentHashMap.contains __do_lift.foreignVarMap { expr := e })

def Lean.Meta.Grind.Arith.Cutsat.foreignTermOrLit? (e : Expr) : GoalM (Option ForeignType)

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.getForeignVars (t : ForeignType) : GoalM (PArray Expr)

Equations

• Lean.Meta.Grind.Arith.Cutsat.getForeignVars t = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.get' pure ((Lean.PersistentHashMap.find? __do_lift.foreignVars t).getD { })

def Lean.Meta.Grind.Arith.Cutsat.ForeignType.denoteType : ForeignType → Expr

Equations

• Lean.Meta.Grind.Arith.Cutsat.ForeignType.nat.denoteType = Lean.mkConst `Nat