summary |
shortlog | log |
commit |
commitdiff |
tree
first ⋅ prev ⋅ next
Anders [Mon, 23 Mar 2015 14:59:03 +0000 (15:59 +0100)]
Add evaluation of Glue and GlueElem
Simon Huber [Fri, 20 Mar 2015 14:21:28 +0000 (15:21 +0100)]
fixed compLine; improved error msg for @@
Simon Huber [Fri, 20 Mar 2015 13:54:48 +0000 (14:54 +0100)]
dont crash the resolver if expression could not be resolved
Anders [Fri, 20 Mar 2015 10:08:48 +0000 (11:08 +0100)]
Update .gitignore
Anders [Fri, 20 Mar 2015 10:08:18 +0000 (11:08 +0100)]
Fix printing of formulas in AppFormula
Anders [Fri, 20 Mar 2015 09:41:17 +0000 (10:41 +0100)]
Add support for multiple bindings of dimensions
Anders [Fri, 20 Mar 2015 09:30:44 +0000 (10:30 +0100)]
Fix printing of systems
Anders [Fri, 20 Mar 2015 09:30:07 +0000 (10:30 +0100)]
Fix bug in gensym and add Square
Anders [Thu, 19 Mar 2015 17:53:47 +0000 (18:53 +0100)]
Finish implementing comp
Anders [Thu, 19 Mar 2015 16:14:21 +0000 (17:14 +0100)]
Parsing of systems
Anders [Thu, 19 Mar 2015 15:25:55 +0000 (16:25 +0100)]
Started adding comp
Simon Huber [Thu, 19 Mar 2015 13:11:31 +0000 (14:11 +0100)]
the endpoints of a path should match the Id arguments; inferType
Simon Huber [Thu, 19 Mar 2015 11:46:51 +0000 (12:46 +0100)]
throw out Binder
Simon Huber [Thu, 19 Mar 2015 10:40:47 +0000 (11:40 +0100)]
time to wake up
Simon Huber [Thu, 19 Mar 2015 09:55:04 +0000 (10:55 +0100)]
reintroduced Convertible typeclass; fixed conv for formulas
Simon Huber [Thu, 19 Mar 2015 09:35:55 +0000 (10:35 +0100)]
fixed support for Env
Anders Mörtberg [Thu, 19 Mar 2015 08:59:30 +0000 (09:59 +0100)]
Start adding inferType
Anders Mörtberg [Thu, 19 Mar 2015 07:58:38 +0000 (08:58 +0100)]
Add 0 and 1 to parser and resolver
Anders Mörtberg [Thu, 19 Mar 2015 07:58:26 +0000 (08:58 +0100)]
Use checkPath when checking IdP
Anders Mörtberg [Thu, 19 Mar 2015 07:58:05 +0000 (08:58 +0100)]
Add .gitignore
Anders Mörtberg [Thu, 19 Mar 2015 07:15:30 +0000 (08:15 +0100)]
Names are now strings
Anders Mörtberg [Thu, 19 Mar 2015 06:36:46 +0000 (07:36 +0100)]
Add J
Anders Mörtberg [Thu, 19 Mar 2015 06:36:29 +0000 (07:36 +0100)]
Fix a typo in the parser
Simon Huber [Wed, 18 Mar 2015 23:54:52 +0000 (00:54 +0100)]
added transport
Simon Huber [Wed, 18 Mar 2015 23:15:57 +0000 (00:15 +0100)]
show transport like we parse it; whitespace
Simon Huber [Wed, 18 Mar 2015 22:48:11 +0000 (23:48 +0100)]
added app of a formula
Anders [Wed, 18 Mar 2015 17:20:06 +0000 (18:20 +0100)]
Add Id, Path, AppFormula and Trans.
funExt is working!
Anders [Wed, 18 Mar 2015 10:57:06 +0000 (11:57 +0100)]
Add Connections
Anders [Wed, 18 Mar 2015 10:53:37 +0000 (11:53 +0100)]
Rename to cubical
Anders [Wed, 18 Mar 2015 10:50:30 +0000 (11:50 +0100)]
Start adding Id types
Anders [Tue, 17 Mar 2015 13:59:45 +0000 (14:59 +0100)]
Remove Neutral data type
Anders Mörtberg [Wed, 18 Mar 2015 09:15:33 +0000 (10:15 +0100)]
Clean Resolver
Anders [Mon, 16 Mar 2015 16:09:28 +0000 (17:09 +0100)]
Start working on cubical type theory
Anders [Thu, 26 Feb 2015 13:35:29 +0000 (14:35 +0100)]
Initial commit
mortberg [Thu, 26 Feb 2015 13:27:28 +0000 (14:27 +0100)]
Initial commit
projects / cubicaltt.git / log