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]

Properties

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.5), directory (>=1.2), filepath (>=1.3), 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
UploadedSun Apr 27 14:45:14 UTC 2014 by AndersMortberg
DistributionsNixOS:0.2.0
Downloads743 total (35 in last 30 days)
Votes
0 []
StatusDocs not available [build log]
All reported builds failed as of 2015-05-18 [all 2 reports]

Downloads

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 https://github.com/simhu/bnfc 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: