- 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.
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 : α)
:
Equations
- Lean.runMetaEval env opts a = IO.FS.withIsolatedStreams (liftM (EIO.toBaseIO (Lean.MetaEval.eval env opts a false)))