class Lean.Meta.Sym.Arith.MonadGetVar (m : Type → Type) : Type

Read a variable's Lean expression by index. Used by DenoteExpr and diagnostics (PP).

• getVar : Var → m Expr

@[implicit_reducible, always_inline]

instance Lean.Meta.Sym.Arith.instMonadGetVarOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetVar m] : MonadGetVar n

Equations

• Lean.Meta.Sym.Arith.instMonadGetVarOfMonadLift m n = { getVar := fun (x : Lean.Grind.CommRing.Var) => liftM (Lean.Meta.Sym.Arith.getVar x) }

class Lean.Meta.Sym.Arith.MonadMkVar (m : Type → Type) : Type

Create or lookup a variable for a Lean expression. Used by reification.

• mkVar : Expr → m Var

@[implicit_reducible, always_inline]

instance Lean.Meta.Sym.Arith.instMonadMkVarOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadMkVar m] : MonadMkVar n

Equations

• Lean.Meta.Sym.Arith.instMonadMkVarOfMonadLift m n = { mkVar := fun (e : Lean.Expr) => liftM (Lean.Meta.Sym.Arith.mkVar e) }