lean-bindings-0.1: Haskell bindings to the Lean Theorem Prover.

Copyright(c) Galois Inc, 2015
LicenseApache-2
Maintainerjhendrix@galois.com, lcasburn@galois.com
Safe HaskellTrustworthy
LanguageHaskell98

Language.Lean.Module

Description

Declarations for importing and exporting modules and accessing Lean paths

Synopsis

Documentation

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

Import the given module names into the lean environment

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

Export the lean environment to a path.

stdPath :: String Source

Path to lean standard library (extracted from LEAN_PATH)

hottPath :: String Source

Path to lean hott library (extrcted from HLEAN_PATH)