class Lean.MetaEval (α : Type u) : Type u

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

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.

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

Equations

• Lean.instMetaEval = { eval := fun env x a hideUnit => do Lean.Eval.eval (fun x => a) hideUnit pure env }

def Lean.runMetaEval {α : Type u} [inst : 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)))