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} [Lean.Eval α] : Lean.MetaEval α

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