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.0, 0.1.1, 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
UploadedThu Dec 19 16:53:15 UTC 2013 by AndersMortberg

Downloads

Maintainers' corner

For package maintainers and hackage trustees

Readme for cubical-0.1.0

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 cubical do cabal configure cabal build 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: