compileTimeSearchPath%

Stream: std4

[Scott Morrison]

Can we put

/--
Term elaborator that retrieves the current `SearchPath`.

This can only be used in files that are compiled locally.
(That is, if used in an imported file it will embed the search path from whichever machine
compiled the `.olean`.)
-/
elab "compileTimeSearchPath%" : term =>
  return toExpr (← searchPathRef.get)

in Std? I want it in multiple locations (and it was being duplicated in Mathlib), so upstreaming seems natural.

[Mario Carneiro]

it should be snake cased

[Scott Morrison]

Okay, this is in std4#222, but that is stacked on top of std4#221.