instance Lean.Meta.Linear.Nat.instReprExpr_lean : Repr Nat.Linear.Expr

instance Lean.Meta.Linear.Nat.instReprExprCnstr_lean : Repr Nat.Linear.ExprCnstr

Equations

• Lean.Meta.Linear.Nat.instReprExprCnstr_lean = { reprPrec := Lean.Meta.Linear.Nat.reprExprCnstr✝ }

instance Lean.Meta.Linear.Nat.instReprPolyCnstr_lean : Repr Nat.Linear.PolyCnstr

@[reducible, inline]

abbrev Lean.Meta.Linear.Nat.LinearExpr : Type

Equations

• Lean.Meta.Linear.Nat.LinearExpr = Nat.Linear.Expr

@[reducible, inline]

abbrev Lean.Meta.Linear.Nat.LinearCnstr : Type

Equations

• Lean.Meta.Linear.Nat.LinearCnstr = Nat.Linear.ExprCnstr

@[reducible, inline]

abbrev Lean.Meta.Linear.Nat.PolyExpr : Type

def Lean.Meta.Linear.Nat.LinearExpr.toExpr (e : Lean.Meta.Linear.Nat.LinearExpr) : Lean.Expr

instance Lean.Meta.Linear.Nat.instToExprLinearExpr : Lean.ToExpr Lean.Meta.Linear.Nat.LinearExpr

def Lean.Meta.Linear.Nat.LinearCnstr.toExpr (c : Lean.Meta.Linear.Nat.LinearCnstr) : Lean.Expr

instance Lean.Meta.Linear.Nat.instToExprLinearCnstr : Lean.ToExpr Lean.Meta.Linear.Nat.LinearCnstr

Equations

• Lean.Meta.Linear.Nat.instToExprLinearCnstr = { toExpr := fun (a : Lean.Meta.Linear.Nat.LinearCnstr) => a.toExpr, toTypeExpr := Lean.mkConst `Nat.Linear.ExprCnstr }

def Lean.Meta.Linear.Nat.LinearExpr.toArith (ctx : Array Lean.Expr) (e : Lean.Meta.Linear.Nat.LinearExpr) : Lean.MetaM Lean.Expr

def Lean.Meta.Linear.Nat.LinearCnstr.toArith (ctx : Array Lean.Expr) (c : Lean.Meta.Linear.Nat.LinearCnstr) : Lean.MetaM Lean.Expr

Equations

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

structure Lean.Meta.Linear.Nat.ToLinear.State : Type

• varMap : Lean.Meta.KExprMap Nat
• vars : Array Lean.Expr

@[reducible, inline]

abbrev Lean.Meta.Linear.Nat.ToLinear.M (α : Type) : Type

Equations

• Lean.Meta.Linear.Nat.ToLinear.M = StateRefT' IO.RealWorld Lean.Meta.Linear.Nat.ToLinear.State Lean.MetaM

def Lean.Meta.Linear.Nat.ToLinear.addAsVar (e : Lean.Expr) : Lean.Meta.Linear.Nat.ToLinear.M Lean.Meta.Linear.Nat.LinearExpr

partial def Lean.Meta.Linear.Nat.ToLinear.toLinearExpr (e : Lean.Expr) : Lean.Meta.Linear.Nat.ToLinear.M Lean.Meta.Linear.Nat.LinearExpr

partial def Lean.Meta.Linear.Nat.ToLinear.toLinearExpr.visit (e : Lean.Expr) : Lean.Meta.Linear.Nat.ToLinear.M Lean.Meta.Linear.Nat.LinearExpr

def Lean.Meta.Linear.Nat.ToLinear.toLinearCnstr? (e : Lean.Expr) : Lean.Meta.Linear.Nat.ToLinear.M (Option Lean.Meta.Linear.Nat.LinearCnstr)

Equations

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

def Lean.Meta.Linear.Nat.ToLinear.run {α : Type} (x : Lean.Meta.Linear.Nat.ToLinear.M α) : Lean.MetaM (α × Array Lean.Expr)

def Lean.Meta.Linear.Nat.toContextExpr (ctx : Array Lean.Expr) : Lean.Expr

def Lean.Meta.Linear.Nat.reflTrue : Lean.Expr

Equations

• Lean.Meta.Linear.Nat.reflTrue = Lean.mkApp2 (Lean.mkConst `Eq.refl [Lean.levelOne]) (Lean.mkConst `Bool) (Lean.mkConst `Bool.true)