The lean-bindings package

[maintain]

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.

Properties

Version0.1
Dependenciesbase (>=4.6 && <5), bytestring, integer-gmp, integer-simple, lens, text [details]
LicenseApache-2.0
AuthorJoe Hendrix
Maintainerjhendrix@galois.com
CategoryLanguage, Formal Languages, Foreign, FFI, Theorem Provers
Source repositoryhead: git clone https://github.com/GaloisInc/lean-haskell-bindings.git
UploadedWed Sep 9 21:46:33 UTC 2015 by jhendrix

Modules

[Index]

Flags

NameDescriptionDefaultType
use-integer-simpleUse this when compiling using a ghc that uses integer-simple instead of integer-gmp.DisabledAutomatic

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainers' corner

For package maintainers and hackage trustees