projects
/
cubicaltt.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cubicaltt.git
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
2015-03-24
Simon Huber
bugfix in trans
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
bugfix for act on a path
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
added compElem and elimComp (still buggy)
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
pairs now associate to the right
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
lemTest not in prelude..
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
added simplify for Trans and Comp
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
removed Map. here and there
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
fixed bug; switched a with b in hiso
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
enhanced and renamed emacs mode
commit
|
commitdiff
|
tree
|
snapshot
2015-03-23
Anders
Finish adding glue
commit
|
commitdiff
|
tree
|
snapshot
2015-03-23
Anders
Add evaluation of Glue and GlueElem
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Simon Huber
fixed compLine; improved error msg for @@
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Simon Huber
dont crash the resolver if expression could not be...
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Update .gitignore
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Fix printing of formulas in AppFormula
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Add support for multiple bindings of dimensions
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Fix printing of systems
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Fix bug in gensym and add Square
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders
Finish implementing comp
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders
Parsing of systems
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders
Started adding comp
commit
|
commitdiff
|
tree
|
snapshot
next