Documentation

Lean.Eval

source
class Lean.MetaEval (α : Type u) :
Type u
Instances
source
instance Lean.instMetaEval {α : Type u} [inst : Lean.Eval α] :
Lean.MetaEval α
Equations
  • Lean.instMetaEval = { eval := fun env opts a hideUnit => do Lean.Eval.eval (fun x => a) hideUnit pure env }
source
def Lean.runMetaEval {α : Type u} [inst : Lean.MetaEval α] (env : Lean.Environment) (opts : Lean.Options) (a : α) :
IO (String × Except IO.Error Lean.Environment)
Equations