class Lean.MetaEval (α : Type u) : 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.

• eval : Lean.Environment → Lean.Options → α → Bool → IO Lean.Environment

instance Lean.instMetaEvalOfEval {α : Type u} [Lean.Eval α] : Lean.MetaEval α

Equations

• Lean.instMetaEvalOfEval = { eval := fun (env : Lean.Environment) (x : Lean.Options) (a : α) (hideUnit : Bool) => do Lean.Eval.eval (fun (x : Unit) => a) hideUnit pure env }

def Lean.runMetaEval {α : Type u} [Lean.MetaEval α] (env : Lean.Environment) (opts : Lean.Options) (a : α) : IO (String × Except IO.Error Lean.Environment)

Equations

• Lean.runMetaEval env opts a = IO.FS.withIsolatedStreams (liftM (EIO.toBaseIO (Lean.MetaEval.eval env opts a false)))