| 2015-04-19 |
coquand | any isomorphism is an equivalence |
commit | commitdiff | tree | snapshot |
| 2015-04-19 |
coquand | if A and B are isomorphic, set A -> set B, normal form |
commit | commitdiff | tree | snapshot |
| 2015-04-19 |
coquand | if A and B are isomorphic, prop A -> prop B, normal... |
commit | commitdiff | tree | snapshot |
| 2015-04-19 |
coquand | result on equivalence of fibers |
commit | commitdiff | tree | snapshot |
| 2015-04-19 |
coquand | new proof of Hedberg's theorem |
commit | commitdiff | tree | snapshot |
| 2015-04-17 |
Anders | Fix printing of goals and environments (TODO: Fix ... |
commit | commitdiff | tree | snapshot |
| 2015-04-17 |
Anders | Rewrite app and support using case-of |
commit | commitdiff | tree | snapshot |
| 2015-04-17 |
Anders | Use Except instead or Error |
commit | commitdiff | tree | snapshot |
| 2015-04-17 |
Anders | Remove tabs |
commit | commitdiff | tree | snapshot |
| 2015-04-17 |
Anders Mörtberg | Only show second part of VPi x (VLam ...) |
commit | commitdiff | tree | snapshot |
| 2015-04-17 |
Anders Mörtberg | Also normalize the type of lambdas and print VPi nicer |
commit | commitdiff | tree | snapshot |
| 2015-04-17 |
Anders Mörtberg | Use showTer1 to print closures |
commit | commitdiff | tree | snapshot |
| 2015-04-17 |
Anders Mörtberg | Fix uafunext2 |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Anders | Remove some incidentally commited holes |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Anders | Reintroduce _ in identifier again |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Simon Huber | reintroduce nicer mkVar |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Simon Huber | keep name if we have it when generating a fresh name |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Simon Huber | change mkVar back to how it was |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Anders Mörtberg | Add indentation to Checking and start changing mkVar... |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Anders Mörtberg | Only print File loaded if file type checks |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Anders Mörtberg | Change gensym |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Anders Mörtberg | Make holes print the context |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Anders Mörtberg | Trailing whitespace |
commit | commitdiff | tree | snapshot |
| 2015-04-16 |
Anders Mörtberg | Fix undefined |
commit | commitdiff | tree | snapshot |
| 2015-04-15 |
Anders | Finish example of integers as a HIT |
commit | commitdiff | tree | snapshot |
| 2015-04-15 |
Anders | Remove some code from ex1 |
commit | commitdiff | tree | snapshot |
| 2015-04-15 |
Anders | Fix bug in type checker for HITs |
commit | commitdiff | tree | snapshot |
| 2015-04-15 |
Anders | Fix undefined |
commit | commitdiff | tree | snapshot |
| 2015-04-15 |
Anders Mörtberg | Remove VUndef |
commit | commitdiff | tree | snapshot |
| 2015-04-15 |
Anders Mörtberg | Add very simple support for holes |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
Anders Mörtberg | Make list compile |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
Anders Mörtberg | Make undefined only occur as a declaration so that... |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
Anders Mörtberg | Undef is neutral (but there is an issue with inferType... |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
Anders Mörtberg | Start defining integers as a HIT and proving that they... |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
Anders | Fix printing of fst, snd and lambdas |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
Anders | Update the description in demo.ctt |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
coquand | added some lines in ex1.ctt |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
coquand | added some lines in ex1.ctt |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
coquand | small change in helix.ctt |
commit | commitdiff | tree | snapshot |
| 2015-04-14 |
coquand | one example with constant functions |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders Mörtberg | Fix bug in Resolver |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders Mörtberg | Remove contr from equiv |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Simon Huber | license should include names |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
coquand | small modification in the file susp |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders Mörtberg | Update help message |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders Mörtberg | Update README |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders Mörtberg | Move stream to experiments |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Add dependency graph script |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Update README |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Lots of cleaning in the examples |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Add equiv and uafunext2 |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Reorganized and cleaned some examples |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Update README |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Fix README |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Update README |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Anders | Update the README and examples |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Simon Huber | demo from the proglog talk |
commit | commitdiff | tree | snapshot |
| 2015-04-13 |
Simon Huber | use smart fst/snd in act |
commit | commitdiff | tree | snapshot |
| 2015-04-12 |
Simon Huber | added thierrys examples (funext from univalence,helix) |
commit | commitdiff | tree | snapshot |
| 2015-04-11 |
Simon Huber | fixing use of isNeutral |
commit | commitdiff | tree | snapshot |
| 2015-04-10 |
Anders | Fix parsing of trans, comp, etc. |
commit | commitdiff | tree | snapshot |
| 2015-04-10 |
Anders | Explicitly pass around the history |
commit | commitdiff | tree | snapshot |
| 2015-04-10 |
mortberg | Merge pull request #6 from nad/master |
commit | commitdiff | tree | snapshot |
| 2015-04-09 |
Anders Mörtberg | Start the proof that ua implies funext |
commit | commitdiff | tree | snapshot |
| 2015-04-09 |
Nils Anders... | Proved (?) that equality coincides with bisimilarity. |
commit | commitdiff | tree | snapshot |
| 2015-04-09 |
Anders | Clean examples |
commit | commitdiff | tree | snapshot |
| 2015-04-09 |
Anders | Add normalization function |
commit | commitdiff | tree | snapshot |
| 2015-04-09 |
Simon Huber | funext from interval |
commit | commitdiff | tree | snapshot |
| 2015-04-08 |
Simon Huber | don't crash the main loop if error in eval |
commit | commitdiff | tree | snapshot |
| 2015-04-08 |
Simon Huber | split annotation is now the type not the family; typo... |
commit | commitdiff | tree | snapshot |
| 2015-04-08 |
Simon Huber | evaluate undefined into a closure |
commit | commitdiff | tree | snapshot |
| 2015-04-08 |
Simon Huber | function should be known in def (for general recursion) |
commit | commitdiff | tree | snapshot |
| 2015-04-08 |
Anders | Cleaning |
commit | commitdiff | tree | snapshot |
| 2015-04-08 |
Simon Huber | added thierrys adapted files |
commit | commitdiff | tree | snapshot |
| 2015-04-07 |
Simon Huber | improve show of a sum |
commit | commitdiff | tree | snapshot |
| 2015-04-07 |
Simon Huber | analogous fix for pathUniv |
commit | commitdiff | tree | snapshot |
| 2015-04-07 |
Simon Huber | bugfix in pathUnivTrans |
commit | commitdiff | tree | snapshot |
| 2015-03-31 |
Simon Huber | reintroduce faceEnv |
commit | commitdiff | tree | snapshot |
| 2015-03-31 |
Anders | Cleaned and simplified type checker |
commit | commitdiff | tree | snapshot |
| 2015-03-30 |
Simon Huber | bugfix in simplify, conv; extended prelude |
commit | commitdiff | tree | snapshot |
| 2015-03-29 |
Anders | Fix parsing of /\ |
commit | commitdiff | tree | snapshot |
| 2015-03-29 |
Anders Mörtberg | Fix error message when path constructors are written... |
commit | commitdiff | tree | snapshot |
| 2015-03-28 |
Anders Mörtberg | Cleaning |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | Update Makefile |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | readme |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | fix readme |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | fix readme |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | Update readme |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | Examples |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | app for VCompElem and VElimComp |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | Fix conversion of formulas |
commit | commitdiff | tree | snapshot |
| 2015-03-27 |
Anders | Fix isNeutral |
commit | commitdiff | tree | snapshot |
| 2015-03-26 |
Anders | Add more tests |
commit | commitdiff | tree | snapshot |
| 2015-03-26 |
Anders | Fix a bug in eqLemma |
commit | commitdiff | tree | snapshot |
| 2015-03-26 |
Anders | Add the circle (there is a bug) |
commit | commitdiff | tree | snapshot |
| 2015-03-26 |
Anders | Finish adding HITs |
commit | commitdiff | tree | snapshot |
| 2015-03-26 |
Anders | Add squeeze, fix some bugs and optimize(?) transport |
commit | commitdiff | tree | snapshot |
| 2015-03-26 |
Simon Huber | moved transGlue; typo in compGlue |
commit | commitdiff | tree | snapshot |
| 2015-03-25 |
Anders | Add HITs (parsing and resolver missing) |
commit | commitdiff | tree | snapshot |
| 2015-03-24 |
Simon Huber | examples |
commit | commitdiff | tree | snapshot |
| next |
projects / cubicaltt.git / shortlog