Documentation

Lean.Meta.Tactic.LinearArith.Nat.Basic

instance Lean.Meta.Linear.Nat.instReprExpr:

Repr Nat.Linear.Expr

Equations

Lean.Meta.Linear.Nat.instReprExpr = { reprPrec := [anonymous] }

instance Lean.Meta.Linear.Nat.instReprExprCnstr:

Repr Nat.Linear.ExprCnstr

Equations

Lean.Meta.Linear.Nat.instReprExprCnstr = { reprPrec := [anonymous] }

instance Lean.Meta.Linear.Nat.instReprPolyCnstr:

Repr Nat.Linear.PolyCnstr

Equations

Lean.Meta.Linear.Nat.instReprPolyCnstr = { reprPrec := [anonymous] }

@[inline]

abbrev Lean.Meta.Linear.Nat.LinearExpr:

Type

Equations

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

@[inline]

abbrev Lean.Meta.Linear.Nat.LinearCnstr:

Type

Equations

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

@[inline]

abbrev Lean.Meta.Linear.Nat.PolyExpr:

Type

Equations

Lean.Meta.Linear.Nat.PolyExpr = Nat.Linear.Poly

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

Equations

One or more equations did not get rendered due to their size.
Lean.Meta.Linear.Nat.LinearExpr.toExpr (Nat.Linear.Expr.num v) = Lean.mkApp (Lean.mkConst `Nat.Linear.Expr.num) (Lean.mkNatLit v)
Lean.Meta.Linear.Nat.LinearExpr.toExpr (Nat.Linear.Expr.var i) = Lean.mkApp (Lean.mkConst `Nat.Linear.Expr.var) (Lean.mkNatLit i)
Lean.Meta.Linear.Nat.LinearExpr.toExpr (Nat.Linear.Expr.mulL k a) = Lean.mkApp2 (Lean.mkConst `Nat.Linear.Expr.mulL) (Lean.mkNatLit k) (Lean.Meta.Linear.Nat.LinearExpr.toExpr a)
Lean.Meta.Linear.Nat.LinearExpr.toExpr (Nat.Linear.Expr.mulR a k) = Lean.mkApp2 (Lean.mkConst `Nat.Linear.Expr.mulR) (Lean.Meta.Linear.Nat.LinearExpr.toExpr a) (Lean.mkNatLit k)

instance Lean.Meta.Linear.Nat.instToExprLinearExpr:

Lean.ToExpr Lean.Meta.Linear.Nat.LinearExpr

Equations

Lean.Meta.Linear.Nat.instToExprLinearExpr = { toExpr := fun a => Lean.Meta.Linear.Nat.LinearExpr.toExpr a, toTypeExpr := Lean.mkConst `Nat.Linear.Expr }

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

Equations

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

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.toExpr a, 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

Equations

One or more equations did not get rendered due to their size.
Lean.Meta.Linear.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.num v) = pure (Lean.mkNatLit v)
Lean.Meta.Linear.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.var i) = pure (Array.getOp ctx i)
Lean.Meta.Linear.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.mulL k a) = do let a ← Lean.Meta.Linear.Nat.LinearExpr.toArith ctx a Lean.Meta.mkMul (Lean.mkNatLit k) a
Lean.Meta.Linear.Nat.LinearExpr.toArith ctx (Nat.Linear.Expr.mulR a k) = do let a ← Lean.Meta.Linear.Nat.LinearExpr.toArith ctx a Lean.Meta.mkMul a (Lean.mkNatLit k)

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

@[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

Equations

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

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

partial def Lean.Meta.Linear.Nat.ToLinear.toLinearCnstr? (e : Lean.Expr) :

Lean.Meta.Linear.Nat.ToLinear.M (Option Lean.Meta.Linear.Nat.LinearCnstr)

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

Lean.MetaM (α × Array Lean.Expr)

Equations

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

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.Linear.Nat.toContextExpr ctx = Lean.Meta.mkListLit (Lean.mkConst `Nat) (Array.toList ctx)

def Lean.Meta.Linear.Nat.reflTrue:

Equations

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