HepLean Documentation
Lake
.
DSL
.
Extensions
Search
Google site search
return to top
source
Imports
Init
Lean.Environment
Imported by
Lake
.
dirExt
Lake
.
optsExt
source
opaque
Lake
.
dirExt
:
Lean.EnvExtension
(
Option
Lake.FilePath
)
source
opaque
Lake
.
optsExt
:
Lean.EnvExtension
(
Option
(
Lake.NameMap
String
)
)