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

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