The cubical package

[maintain]

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


[Skip to ReadMe]

Properties

Versions0.1.0, 0.1.1, 0.1.2, 0.1.2, 0.2.0
Dependenciesarray (>=0.4), base (>=4.5 && <5), BNFC (>=2.6), directory (>=1.2), haskeline (>=0.7), mtl (>=2.1), transformers (>=0.3) [details]
LicenseMIT
AuthorCyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
Maintainermortberg@chalmers.se
CategoryDependent Types
Home pagehttps://github.com/simhu/cubical
Executablescubical
UploadedWed Dec 25 10:51:57 UTC 2013 by AndersMortberg

Downloads

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: