cubicaltt.git
2016-01-15 Anders MörtbergFinish the last undefined in setquot
2016-01-15 Anders Mörtberg"fix" bug
2016-01-15 Simon HuberBugfix in inferType
2016-01-15 Anders Mörtbergsetquot is a set
2016-01-15 Anders Mörtbergone less undefined
2016-01-15 Anders Mörtbergsquash some admits
2016-01-14 Anders Mörtbergminor changes
2016-01-14 Anders Mörtbergmore on setquot. on the way to define an equality test...
2016-01-14 Anders Mörtbergadd nlem1
2016-01-14 Anders MörtbergChange printing of environments
2016-01-14 Anders Mörtbergrename sig to Sigma and make setquot compile
2016-01-14 Anders Mörtbergmake bool compile and move tests using univalence for...
2016-01-14 Simon HuberBugfix in compU and compGlue
2016-01-12 Simon HuberBugfix by Fabian Ruch
2016-01-09 Anders Mörtbergfix bug
2016-01-08 Anders Mörtbergcleaning
2016-01-07 Anders Mörtbergcomment gradLemmaU
2016-01-07 Anders Mörtbergremove @@@
2016-01-07 Anders Mörtbergdont write to a file
2016-01-07 Anders Mörtberg"_" in constPath again
2016-01-05 Anders Mörtberguse compConstLine
2016-01-05 Anders Mörtbergadd the huge normal form of corrUniv which trigger...
2016-01-05 Anders Mörtbergremove a space in a comment
2016-01-05 Anders Mörtbergchange constPath to avoid strange bug
2016-01-05 Anders Mörtbergcomment
2016-01-05 Anders Mörtbergadd parsing of ! in beginning of idents
2016-01-05 Anders Mörtbergremove all <_>
2016-01-05 Anders Mörtbergchange printing of compU
2016-01-04 coquandadded an example with ordinals
2016-01-04 Anders MörtbergMore cleaning
2016-01-04 Anders MörtbergAdd bool example to univalence.ctt
2016-01-04 Anders MörtbergCleaning and removal of duplicate code. Put all proofs...
2016-01-04 Anders MörtbergRefactoring and move old code on equivalences to experi...
2015-12-31 Anders MörtbergMake aim.ctt compile
2015-12-31 Anders MörtbergMerge branch 'compU'
2015-12-31 Anders MörtbergMerge branch 'testUniv'
2015-12-31 Anders Mörtbergupdate aim.ctt
2015-12-30 Anders Mörtbergadd standard formulation of univalence
2015-12-30 coquandan example of normal form
2015-12-29 coquandupdated collection
2015-12-29 coquandsmall change
2015-12-29 coquandupdated sigma, not use of J
2015-12-29 coquandupdated multS1
2015-12-29 coquandcircle now works with this version of univalence
2015-12-27 coquandchanged compU
2015-12-27 coquandsimple tests for univalence
2015-12-27 coquandneutral for compU
2015-12-26 coquandMakefile
2015-12-26 coquandother proof of univalence
2015-12-26 coquandcorrected Eval
2015-12-26 coquandan example where we type-checked a normal form
2015-12-26 coquandproof of univalence?
2015-12-26 coquandunivalence
2015-12-26 coquandproof of univalence
2015-12-26 coquandupdated testContr
2015-12-22 coquandsome lemmas about contractible types
2015-12-19 coquandtestEquiv
2015-12-19 coquandsimplified transIdFun
2015-12-19 coquandsimpler version of idToId in testEquiv
2015-12-19 coquandtestEquiv
2015-12-19 coquandsimplified transIdFun
2015-12-18 coquandsimpler version of idToId in testEquiv
2015-12-18 Anders Mörtbergalternative definition of equivalences
2015-12-17 Simon HuberFixed eqToEquiv
2015-12-16 Simon HuberSwitched back to equiv, simplified glue
2015-12-15 Simon HuberBugfix for type checking glueElems by Fabian Ruch
2015-12-14 Simon HuberEfficient @@ for fresh names
2015-12-14 Simon HuberSimplified pathComp
2015-12-11 Anders Mörtbergstart working on hz
2015-12-11 Anders MörtbergClean setquot
2015-12-09 Anders Mörtbergadd IdPathTest1
2015-12-04 Anders Mörtbergminor modification to foo
2015-12-04 Anders Mörtberganother small test
2015-12-04 Anders Mörtbergchange es' to es, not sure if this is correct...
2015-12-04 Anders MörtbergSimpler version of gradlemmaU
2015-12-04 Anders Mörtbergminor changes
2015-12-04 Anders MörtbergAdd the missing line in comp!
2015-12-04 Anders Mörtberganother example
2015-12-04 Anders Mörtbergremove reglarity
2015-12-04 Anders Mörtbergadd a shrink function that can be used to not print...
2015-12-04 Anders MörtbergAdd VCompU to normal and conv
2015-12-04 Anders MörtbergAdd some test of normal forms
2015-12-04 Anders MörtbergReintroduce compU
2015-12-03 Anders Mörtbergadd a short version of setquot
2015-12-02 Anders MörtbergProve direct version of uahp
2015-12-02 Anders Mörtbergfix comment
2015-12-02 Anders MörtbergCleaning
2015-12-02 Anders Mörtbergfinish setquot example
2015-12-02 Anders Mörtbergprove that bool is a set
2015-12-02 Anders Mörtbergprove that hProp is a set
2015-12-02 Anders Mörtbergprove uahp
2015-12-01 Anders Mörtbergsetquot
2015-11-26 Simon HuberAnother formulation of univalence
2015-11-19 Anders Mörtbergindentation
2015-11-19 Anders MörtbergAdd a test that of a simple example where Coq gets...
2015-10-26 Anders MörtbergFix printing of Pi types
2015-10-26 Anders MörtbergRevert my previous changes to GNUMakefile and add ...
2015-10-26 Anders MörtbergMerge pull request #23 from DanGrayson/improve-Makefile
2015-10-26 Daniel R. Graysonfix makefile for ghc 7.10
2015-10-26 Anders MörtbergUpdate README.md
next