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%")