Only print File loaded if file type checks

Change gensym

Make holes print the context

Trailing whitespace

Fix undefined

Finish example of integers as a HIT

Remove some code from ex1

Fix bug in type checker for HITs

Fix undefined

Remove VUndef

Add very simple support for holes

Make list compile

Make undefined only occur as a declaration so that the type can be inferred

Undef is neutral (but there is an issue with inferType for undef)

Start defining integers as a HIT and proving that they are a set

Fix printing of fst, snd and lambdas

Update the description in demo.ctt

added some lines in ex1.ctt

added some lines in ex1.ctt

small change in helix.ctt

one example with constant functions

Fix bug in Resolver

Remove contr from equiv

license should include names

small modification in the file susp

Update help message

Update README

Move stream to experiments

Add dependency graph script

Update README

Lots of cleaning in the examples

Add equiv and uafunext2

Reorganized and cleaned some examples

Update README

Fix README

Update README

Update the README and examples

demo from the proglog talk

use smart fst/snd in act

added thierrys examples (funext from univalence,helix)

fixing use of isNeutral

Fix parsing of trans, comp, etc.

Explicitly pass around the history

Merge pull request #6 from nad/master

Proved (?) that equality coincides with bisimilarity.

Start the proof that ua implies funext

Proved (?) that equality coincides with bisimilarity.

With help from Thierry Coquand and Simon Huber.

Clean examples

Add normalization function

funext from interval

don't crash the main loop if error in eval

split annotation is now the type not the family; typo in eval fixed

evaluate undefined into a closure

function should be known in def (for general recursion)

Cleaning

added thierrys adapted files

improve show of a sum

analogous fix for pathUniv

bugfix in pathUnivTrans

reintroduce faceEnv

Cleaned and simplified type checker

bugfix in simplify, conv; extended prelude

Fix parsing of /\

Fix error message when path constructors are written without the type in
curly braces

Cleaning

Update Makefile

readme

fix readme

fix readme

Update readme

Examples

app for VCompElem and VElimComp

Fix conversion of formulas

Fix isNeutral

Add more tests

Fix a bug in eqLemma

Add the circle (there is a bug)

Finish adding HITs

Add squeeze, fix some bugs and optimize(?) transport

moved transGlue; typo in compGlue

Add HITs (parsing and resolver missing)

examples

bugfix in trans

bugfix for act on a path

added compElem and elimComp (still buggy)

pairs now associate to the right

lemTest not in prelude..

added simplify for Trans and Comp

removed Map. here and there

fixed bug; switched a with b in hiso

enhanced and renamed emacs mode

Finish adding glue

Add evaluation of Glue and GlueElem

fixed compLine; improved error msg for @@

dont crash the resolver if expression could not be resolved

Update .gitignore

Fix printing of formulas in AppFormula

Add support for multiple bindings of dimensions

Fix printing of systems

Fix bug in gensym and add Square

Finish implementing comp