cubicaltt.git
2015-04-20 Anders MörtbergFix printing of VPi
2015-04-20 Anders MörtbergFix retract
2015-04-20 AndersMake normal print nicer names
2015-04-20 AndersFix printing of @
2015-04-20 AndersAdd quotient example
2015-04-20 AndersSplit higherhit into multiple files
2015-04-20 AndersMerge remote-tracking branch 'origin/higherhits'
2015-04-20 Anders MörtbergFix the way @ binds (it is now like normal application)
2015-04-20 Anders MörtbergFix a TODO in the resolver (the arguments in a path...
2015-04-20 Anders MörtbergFix all the old examples of HITs
2015-04-20 Anders MörtbergRemove the @ in PLabel
2015-04-19 coquandany isomorphism is an equivalence
2015-04-19 coquandif A and B are isomorphic, set A -> set B, normal form
2015-04-19 coquandif A and B are isomorphic, prop A -> prop B, normal...
2015-04-19 coquandresult on equivalence of fibers
2015-04-19 coquandnew proof of Hedberg's theorem
2015-04-18 Simon Hubersome examples
2015-04-18 Simon HuberlookName error msg for debugging
2015-04-18 Simon Huberbugfix in PBranches
2015-04-18 Simon Huberlet the system in a pcon know about all pcons in the sum
2015-04-18 Simon Huberbugfix
2015-04-18 Simon Huberbugfix in resolver
2015-04-18 Simon Huberwip (not working yet)
2015-04-17 AndersFix printing of goals and environments (TODO: Fix ...
2015-04-17 AndersRewrite app and support using case-of
2015-04-17 AndersUse Except instead or Error
2015-04-17 AndersRemove tabs
2015-04-17 Anders MörtbergOnly show second part of VPi x (VLam ...)
2015-04-17 Anders MörtbergAlso normalize the type of lambdas and print VPi nicer
2015-04-17 Anders MörtbergUse showTer1 to print closures
2015-04-17 Anders MörtbergFix uafunext2
2015-04-16 AndersRemove some incidentally commited holes
2015-04-16 AndersReintroduce _ in identifier again
2015-04-16 Simon Huberreintroduce nicer mkVar
2015-04-16 Simon Huberkeep name if we have it when generating a fresh name
2015-04-16 Simon Huberchange mkVar back to how it was
2015-04-16 Anders MörtbergAdd indentation to Checking and start changing mkVar...
2015-04-16 Anders MörtbergOnly print File loaded if file type checks
2015-04-16 Anders MörtbergChange gensym
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...
next