Documentation

Lake.Util.EvalTerm

source
unsafe def Lake.unsafeEvalTerm (α : Type) [Lean.ToExpr α] (term : Lean.Syntax) :
Lean.Elab.TermElabM α
Instances For
    source
    @[implemented_by Lake.unsafeEvalTerm]
    opaque Lake.evalTerm (α : Type) [Lean.ToExpr α] (term : Lean.Syntax) :
    Lean.Elab.TermElabM α

    ToExpr Instances #

    source
    instance Lake.instToExprFilePath :
    Lean.ToExpr Lake.FilePath