The cubical package

[Tags: mit, program]

Cubical implements an experimental simple type checker for type theory with univalence with an evaluator for closed terms.

[Skip to ReadMe]


Versions0.1.0, 0.1.1, 0.1.2, 0.2.0 (info)
Change logNone available
Dependenciesarray (>=0.4), base (>=4.5 && <5), BNFC (>=2.6), directory (>=1.2), haskeline (>=0.7), mtl (>=2.1), transformers (>=0.3) [details]
AuthorCyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
CategoryDependent Types
Home page
UploadedWed Dec 25 10:52:32 UTC 2013 by AndersMortberg
Downloads818 total (15 in last 30 days)
0 []
StatusDocs not available [build log]
All reported builds failed as of 2015-11-17 [all 5 reports]


Maintainers' corner

For package maintainers and hackage trustees

Readme for cubical-0.1.2

CUBICAL ======= Cubical implements an experimental simple type-checker for type theory with univalence with an evaluator for closed terms. INSTALL ------- To install cubical a working Haskell and cabal installation are required. To build cubical go to the main directory and do cabal install To only build (not install) cubical do cabal configure cabal build Alternatively one can also use the Makefile to build the system by typing: make bnfc && make However this requires that the following Haskell packages are installed: mtl, haskeline, directory, BNFC, alex, happy USAGE ----- To run cubical type cubical <filename> In the interaction loop type :h to get a list of available commands. Note that the current directory will be taken as the search path for the imports. OVERVIEW -------- The program is organized as follows: