Language.Lean.Module

Declarations for importing and exporting modules and accessing Lean paths

Documentation

envImport :: IOState tp -> Env -> List Name -> IO Env

Import the given module names into the lean environment

envExport :: Env -> FilePath -> IO ()

Export the lean environment to a path.

stdPath :: String

Path to lean standard library (extracted from LEAN_PATH)

hottPath :: String

Path to lean hott library (extrcted from HLEAN_PATH)