cubicaltt.git
2015-04-16 Anders MörtbergMake holes print the context
2015-04-16 Anders MörtbergTrailing whitespace
2015-04-16 Anders MörtbergFix undefined
2015-04-15 AndersFinish example of integers as a HIT
2015-04-15 AndersRemove some code from ex1
2015-04-15 AndersFix bug in type checker for HITs
2015-04-15 AndersFix undefined
2015-04-15 Anders MörtbergRemove VUndef
2015-04-15 Anders MörtbergAdd very simple support for holes
2015-04-14 Anders MörtbergMake list compile
2015-04-14 Anders MörtbergMake undefined only occur as a declaration so that...
2015-04-14 Anders MörtbergUndef is neutral (but there is an issue with inferType...
2015-04-14 Anders MörtbergStart defining integers as a HIT and proving that they...
2015-04-14 AndersFix printing of fst, snd and lambdas
2015-04-14 AndersUpdate the description in demo.ctt
2015-04-14 coquandadded some lines in ex1.ctt
2015-04-14 coquandadded some lines in ex1.ctt
2015-04-14 coquandsmall change in helix.ctt
2015-04-14 coquandone example with constant functions
2015-04-13 Anders MörtbergFix bug in Resolver
2015-04-13 Anders MörtbergRemove contr from equiv
2015-04-13 Simon Huberlicense should include names
2015-04-13 coquandsmall modification in the file susp
2015-04-13 Anders MörtbergUpdate help message
2015-04-13 Anders MörtbergUpdate README
2015-04-13 Anders MörtbergMove stream to experiments
2015-04-13 AndersAdd dependency graph script
2015-04-13 AndersUpdate README
2015-04-13 AndersLots of cleaning in the examples
2015-04-13 AndersAdd equiv and uafunext2
2015-04-13 AndersReorganized and cleaned some examples
2015-04-13 AndersUpdate README
2015-04-13 AndersFix README
2015-04-13 AndersUpdate README
2015-04-13 AndersUpdate the README and examples
2015-04-13 Simon Huberdemo from the proglog talk
2015-04-13 Simon Huberuse smart fst/snd in act
2015-04-12 Simon Huberadded thierrys examples (funext from univalence,helix)
2015-04-11 Simon Huberfixing use of isNeutral
2015-04-10 AndersFix parsing of trans, comp, etc.
2015-04-10 AndersExplicitly pass around the history
2015-04-10 mortbergMerge pull request #6 from nad/master
2015-04-09 Anders MörtbergStart the proof that ua implies funext
2015-04-09 Nils Anders... Proved (?) that equality coincides with bisimilarity.
2015-04-09 AndersClean examples
2015-04-09 AndersAdd normalization function
2015-04-09 Simon Huberfunext from interval
2015-04-08 Simon Huberdon't crash the main loop if error in eval
2015-04-08 Simon Hubersplit annotation is now the type not the family; typo...
2015-04-08 Simon Huberevaluate undefined into a closure
2015-04-08 Simon Huberfunction should be known in def (for general recursion)
2015-04-08 AndersCleaning
2015-04-08 Simon Huberadded thierrys adapted files
2015-04-07 Simon Huberimprove show of a sum
2015-04-07 Simon Huberanalogous fix for pathUniv
2015-04-07 Simon Huberbugfix in pathUnivTrans
2015-03-31 Simon Huberreintroduce faceEnv
2015-03-31 AndersCleaned and simplified type checker
2015-03-30 Simon Huberbugfix in simplify, conv; extended prelude
2015-03-29 AndersFix parsing of /\
2015-03-29 Anders MörtbergFix error message when path constructors are written...
2015-03-28 Anders MörtbergCleaning
2015-03-27 AndersUpdate Makefile
2015-03-27 Andersreadme
2015-03-27 Andersfix readme
2015-03-27 Andersfix readme
2015-03-27 AndersUpdate readme
2015-03-27 AndersExamples
2015-03-27 Andersapp for VCompElem and VElimComp
2015-03-27 AndersFix conversion of formulas
2015-03-27 AndersFix isNeutral
2015-03-26 AndersAdd more tests
2015-03-26 AndersFix a bug in eqLemma
2015-03-26 AndersAdd the circle (there is a bug)
2015-03-26 AndersFinish adding HITs
2015-03-26 AndersAdd squeeze, fix some bugs and optimize(?) transport
2015-03-26 Simon Hubermoved transGlue; typo in compGlue
2015-03-25 AndersAdd HITs (parsing and resolver missing)
2015-03-24 Simon Huberexamples
2015-03-24 Simon Huberbugfix in trans
2015-03-24 Simon Huberbugfix for act on a path
2015-03-24 Simon Huberadded compElem and elimComp (still buggy)
2015-03-24 Simon Huberpairs now associate to the right
2015-03-24 Simon HuberlemTest not in prelude..
2015-03-24 Simon Huberadded simplify for Trans and Comp
2015-03-24 Simon Huberremoved Map. here and there
2015-03-24 Simon Huberfixed bug; switched a with b in hiso
2015-03-24 Simon Huberenhanced and renamed emacs mode
2015-03-23 AndersFinish adding glue
2015-03-23 AndersAdd evaluation of Glue and GlueElem
2015-03-20 Simon Huberfixed compLine; improved error msg for @@
2015-03-20 Simon Huberdont crash the resolver if expression could not be...
2015-03-20 AndersUpdate .gitignore
2015-03-20 AndersFix printing of formulas in AppFormula
2015-03-20 AndersAdd support for multiple bindings of dimensions
2015-03-20 AndersFix printing of systems
2015-03-20 AndersFix bug in gensym and add Square
2015-03-19 AndersFinish implementing comp
2015-03-19 AndersParsing of systems
2015-03-19 AndersStarted adding comp
next