Documentation

Lean.Eval

class Lean.MetaEval (α : Type u) :

Eval extension that gives access to the current environment & options. The basic Eval class is in the prelude and should not depend on these types.

Instances
    instance Lean.instMetaEval {α : Type u} [Lean.Eval α] :
    Equations
    • Lean.instMetaEval = { eval := fun env x a hideUnit => do Lean.Eval.eval (fun x => a) hideUnit pure env }