unsafe def Lake.unsafeEvalTerm (α : Type) [Lean.ToExpr α] (term : Lean.Syntax) : Lean.Elab.TermElabM α

Equations

• Lake.unsafeEvalTerm α term = Lean.Elab.Term.evalTerm α (Lean.toTypeExpr α) term Lean.DefinitionSafety.unsafe

@[implemented_by Lake.unsafeEvalTerm]

opaque Lake.evalTerm (α : Type) [Lean.ToExpr α] (term : Lean.Syntax) : Lean.Elab.TermElabM α

ToExpr Instances

instance Lake.instToExprFilePath : Lean.ToExpr Lake.FilePath

Equations

• Lake.instToExprFilePath = { toExpr := fun p => Lean.mkApp (Lean.mkConst `System.FilePath.mk) (Lean.toExpr p.toString), toTypeExpr := Lean.mkConst `System.FilePath }