lean-bindings-0.1: Haskell bindings to the Lean Theorem Prover.
This package contains Haskell bindings to the Lean Theorem Prover.
To get started using this library, you should install Lean first,
and then install this library, providing paths to the Lean header
and library via --extra-include-dirs
and --extra-lib-dirs
repectively.
To use this library, we recomend using a qualified import, such as:
import qualified Language.Lean as Lean
The library currently is still a work in progress. To see the current interface, we recommend starting with the documentation for Language.Lean, and consulting the individual module imports there.
- Language
- Language.Lean
- Language.Lean.Decl
- Language.Lean.Env
- Language.Lean.Exception
- Language.Lean.Expr
- Language.Lean.IOS
- Language.Lean.Inductive
- Internal
- Language.Lean.List
- Language.Lean.Module
- Language.Lean.Name
- Language.Lean.Options
- Language.Lean.Typechecker
- Language.Lean.Univ
- Language.Lean