Documentation

Batteries.Lean.Util.Path

compile_time_search_path% term elaborator. #

Use this as searchPathRef.set compile_time_search_path%.

source
instance instToExprFilePath_batteries :
Lean.ToExpr System.FilePath
Equations
  • One or more equations did not get rendered due to their size.
source
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
Instances For