projects
/
cubicaltt.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cubicaltt.git
2015-04-18
Simon Huber
some examples
commit
|
commitdiff
|
tree
|
snapshot
2015-04-18
Simon Huber
lookName error msg for debugging
commit
|
commitdiff
|
tree
|
snapshot
2015-04-18
Simon Huber
bugfix in PBranches
commit
|
commitdiff
|
tree
|
snapshot
2015-04-18
Simon Huber
let the system in a pcon know about all pcons in the sum
commit
|
commitdiff
|
tree
|
snapshot
2015-04-18
Simon Huber
bugfix
commit
|
commitdiff
|
tree
|
snapshot
2015-04-18
Simon Huber
bugfix in resolver
commit
|
commitdiff
|
tree
|
snapshot
2015-04-18
Simon Huber
wip (not working yet)
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
next