The cubical package


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, 0.2.0
Dependenciesarray (>=0.4), base (>=4.5 && <5), BNFC (>=2.5), directory (>=1.2), filepath (>=1.3), haskeline (>=0.7), mtl (>=2.1), transformers (>=0.3) [details]
AuthorCyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
CategoryDependent Types
Home page
UploadedSun Apr 27 14:44:15 UTC 2014 by AndersMortberg


Maintainers' corner

For package maintainers and hackage trustees

Readme for cubical-0.2.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 (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 Note: In order to make the mutual keyword work a patched version of BNFC is needed. To install this download the patched version from and then cabal install it. ###Emacs mode: To install syntax highlighting for cubical files load the cubical.el file into emacs. In order to load it automatically add (load-file "/path/to/cubical.el") (add-to-list 'auto-mode-alist '("\\.cub\\'" . cub-mode)) to your .emacs file. USAGE ----- To run cubical type cubical <filename> To enable the debugging mode add the -d flag. 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: