compile_time_search_path% term elaborator.

Use this as searchPathRef.set compile_time_search_path%.

instance instToExprFilePath : Lean.ToExpr System.FilePath

Equations

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

def «termCompile_time_search_path%» : Lean.ParserDescr

Term elaborator that retrieves the current SearchPath.

Typical usage is searchPathRef.set compile_time_search_path%.

This must not be used in files that are potentially compiled on another machine and then imported. (That is, if used in an imported file it will embed the search path from whichever machine compiled the .olean.)

Equations

• «termCompile_time_search_path%» = Lean.ParserDescr.node `termCompile_time_search_path% 1024 (Lean.ParserDescr.symbol "compile_time_search_path%")