cubicaltt.git
9 years agofunext from interval
Simon Huber [Thu, 9 Apr 2015 11:16:33 +0000 (13:16 +0200)]
funext from interval

9 years agodon't crash the main loop if error in eval
Simon Huber [Wed, 8 Apr 2015 22:42:29 +0000 (00:42 +0200)]
don't crash the main loop if error in eval

9 years agosplit annotation is now the type not the family; typo in eval fixed
Simon Huber [Wed, 8 Apr 2015 20:14:55 +0000 (22:14 +0200)]
split annotation is now the type not the family; typo in eval fixed

9 years agoevaluate undefined into a closure
Simon Huber [Wed, 8 Apr 2015 16:49:10 +0000 (18:49 +0200)]
evaluate undefined into a closure

9 years agofunction should be known in def (for general recursion)
Simon Huber [Wed, 8 Apr 2015 14:41:04 +0000 (16:41 +0200)]
function should be known in def (for general recursion)

9 years agoCleaning
Anders [Wed, 8 Apr 2015 10:27:59 +0000 (12:27 +0200)]
Cleaning

9 years agoadded thierrys adapted files
Simon Huber [Wed, 8 Apr 2015 08:21:02 +0000 (10:21 +0200)]
added thierrys adapted files

9 years agoimprove show of a sum
Simon Huber [Tue, 7 Apr 2015 12:14:51 +0000 (14:14 +0200)]
improve show of a sum

9 years agoanalogous fix for pathUniv
Simon Huber [Tue, 7 Apr 2015 12:12:36 +0000 (14:12 +0200)]
analogous fix for pathUniv

9 years agobugfix in pathUnivTrans
Simon Huber [Tue, 7 Apr 2015 12:05:05 +0000 (14:05 +0200)]
bugfix in pathUnivTrans

9 years agoreintroduce faceEnv
Simon Huber [Tue, 31 Mar 2015 17:53:29 +0000 (19:53 +0200)]
reintroduce faceEnv

9 years agoCleaned and simplified type checker
Anders [Tue, 31 Mar 2015 10:06:04 +0000 (12:06 +0200)]
Cleaned and simplified type checker

9 years agobugfix in simplify, conv; extended prelude
Simon Huber [Mon, 30 Mar 2015 15:06:08 +0000 (17:06 +0200)]
bugfix in simplify, conv; extended prelude

9 years agoFix parsing of /\
Anders [Sun, 29 Mar 2015 18:37:22 +0000 (20:37 +0200)]
Fix parsing of /\

9 years agoFix error message when path constructors are written without the type in
Anders Mörtberg [Sun, 29 Mar 2015 17:05:49 +0000 (19:05 +0200)]
Fix error message when path constructors are written without the type in
curly braces

9 years agoCleaning
Anders Mörtberg [Sat, 28 Mar 2015 08:29:45 +0000 (09:29 +0100)]
Cleaning

9 years agoUpdate Makefile
Anders [Fri, 27 Mar 2015 17:05:09 +0000 (18:05 +0100)]
Update Makefile

9 years agoreadme
Anders [Fri, 27 Mar 2015 16:57:45 +0000 (17:57 +0100)]
readme

9 years agofix readme
Anders [Fri, 27 Mar 2015 16:55:51 +0000 (17:55 +0100)]
fix readme

9 years agofix readme
Anders [Fri, 27 Mar 2015 16:55:14 +0000 (17:55 +0100)]
fix readme

9 years agoUpdate readme
Anders [Fri, 27 Mar 2015 16:53:16 +0000 (17:53 +0100)]
Update readme

9 years agoExamples
Anders [Fri, 27 Mar 2015 16:53:07 +0000 (17:53 +0100)]
Examples

9 years agoapp for VCompElem and VElimComp
Anders [Fri, 27 Mar 2015 16:52:46 +0000 (17:52 +0100)]
app for VCompElem and VElimComp

9 years agoFix conversion of formulas
Anders [Fri, 27 Mar 2015 16:52:26 +0000 (17:52 +0100)]
Fix conversion of formulas

9 years agoFix isNeutral
Anders [Fri, 27 Mar 2015 16:52:09 +0000 (17:52 +0100)]
Fix isNeutral

9 years agoAdd more tests
Anders [Thu, 26 Mar 2015 17:15:04 +0000 (18:15 +0100)]
Add more tests

9 years agoFix a bug in eqLemma
Anders [Thu, 26 Mar 2015 16:41:13 +0000 (17:41 +0100)]
Fix a bug in eqLemma

9 years agoAdd the circle (there is a bug)
Anders [Thu, 26 Mar 2015 15:52:46 +0000 (16:52 +0100)]
Add the circle (there is a bug)

9 years agoFinish adding HITs
Anders [Thu, 26 Mar 2015 15:52:26 +0000 (16:52 +0100)]
Finish adding HITs

9 years agoAdd squeeze, fix some bugs and optimize(?) transport
Anders [Thu, 26 Mar 2015 14:21:45 +0000 (15:21 +0100)]
Add squeeze, fix some bugs and optimize(?) transport

9 years agomoved transGlue; typo in compGlue
Simon Huber [Thu, 26 Mar 2015 11:07:10 +0000 (12:07 +0100)]
moved transGlue; typo in compGlue

9 years agoAdd HITs (parsing and resolver missing)
Anders [Wed, 25 Mar 2015 18:06:44 +0000 (19:06 +0100)]
Add HITs (parsing and resolver missing)

9 years agoexamples
Simon Huber [Tue, 24 Mar 2015 17:19:51 +0000 (18:19 +0100)]
examples

9 years agobugfix in trans
Simon Huber [Tue, 24 Mar 2015 17:18:58 +0000 (18:18 +0100)]
bugfix in trans

9 years agobugfix for act on a path
Simon Huber [Tue, 24 Mar 2015 16:27:58 +0000 (17:27 +0100)]
bugfix for act on a path

9 years agoadded compElem and elimComp (still buggy)
Simon Huber [Tue, 24 Mar 2015 15:00:22 +0000 (16:00 +0100)]
added compElem and elimComp (still buggy)

9 years agopairs now associate to the right
Simon Huber [Tue, 24 Mar 2015 10:41:59 +0000 (11:41 +0100)]
pairs now associate to the right

9 years agolemTest not in prelude..
Simon Huber [Tue, 24 Mar 2015 10:29:44 +0000 (11:29 +0100)]
lemTest not in prelude..

9 years agoadded simplify for Trans and Comp
Simon Huber [Tue, 24 Mar 2015 10:29:13 +0000 (11:29 +0100)]
added simplify for Trans and Comp

9 years agoremoved Map. here and there
Simon Huber [Tue, 24 Mar 2015 10:15:29 +0000 (11:15 +0100)]
removed Map. here and there

9 years agofixed bug; switched a with b in hiso
Simon Huber [Tue, 24 Mar 2015 10:06:28 +0000 (11:06 +0100)]
fixed bug; switched a with b in hiso

9 years agoenhanced and renamed emacs mode
Simon Huber [Tue, 24 Mar 2015 09:59:55 +0000 (10:59 +0100)]
enhanced and renamed emacs mode

9 years agoFinish adding glue
Anders [Mon, 23 Mar 2015 17:13:12 +0000 (18:13 +0100)]
Finish adding glue

9 years agoAdd evaluation of Glue and GlueElem
Anders [Mon, 23 Mar 2015 14:59:03 +0000 (15:59 +0100)]
Add evaluation of Glue and GlueElem

9 years agofixed compLine; improved error msg for @@
Simon Huber [Fri, 20 Mar 2015 14:21:28 +0000 (15:21 +0100)]
fixed compLine; improved error msg for @@

9 years agodont crash the resolver if expression could not be resolved
Simon Huber [Fri, 20 Mar 2015 13:54:48 +0000 (14:54 +0100)]
dont crash the resolver if expression could not be resolved

9 years agoUpdate .gitignore
Anders [Fri, 20 Mar 2015 10:08:48 +0000 (11:08 +0100)]
Update .gitignore

9 years agoFix printing of formulas in AppFormula
Anders [Fri, 20 Mar 2015 10:08:18 +0000 (11:08 +0100)]
Fix printing of formulas in AppFormula

9 years agoAdd support for multiple bindings of dimensions
Anders [Fri, 20 Mar 2015 09:41:17 +0000 (10:41 +0100)]
Add support for multiple bindings of dimensions

9 years agoFix printing of systems
Anders [Fri, 20 Mar 2015 09:30:44 +0000 (10:30 +0100)]
Fix printing of systems

9 years agoFix bug in gensym and add Square
Anders [Fri, 20 Mar 2015 09:30:07 +0000 (10:30 +0100)]
Fix bug in gensym and add Square

9 years agoFinish implementing comp
Anders [Thu, 19 Mar 2015 17:53:47 +0000 (18:53 +0100)]
Finish implementing comp

9 years agoParsing of systems
Anders [Thu, 19 Mar 2015 16:14:21 +0000 (17:14 +0100)]
Parsing of systems

9 years agoStarted adding comp
Anders [Thu, 19 Mar 2015 15:25:55 +0000 (16:25 +0100)]
Started adding comp

9 years agothe endpoints of a path should match the Id arguments; inferType
Simon Huber [Thu, 19 Mar 2015 13:11:31 +0000 (14:11 +0100)]
the endpoints of a path should match the Id arguments; inferType

9 years agothrow out Binder
Simon Huber [Thu, 19 Mar 2015 11:46:51 +0000 (12:46 +0100)]
throw out Binder

9 years agotime to wake up
Simon Huber [Thu, 19 Mar 2015 10:40:47 +0000 (11:40 +0100)]
time to wake up

9 years agoreintroduced Convertible typeclass; fixed conv for formulas
Simon Huber [Thu, 19 Mar 2015 09:55:04 +0000 (10:55 +0100)]
reintroduced Convertible typeclass; fixed conv for formulas

9 years agofixed support for Env
Simon Huber [Thu, 19 Mar 2015 09:35:55 +0000 (10:35 +0100)]
fixed support for Env

9 years agoStart adding inferType
Anders Mörtberg [Thu, 19 Mar 2015 08:59:30 +0000 (09:59 +0100)]
Start adding inferType

9 years agoAdd 0 and 1 to parser and resolver
Anders Mörtberg [Thu, 19 Mar 2015 07:58:38 +0000 (08:58 +0100)]
Add 0 and 1 to parser and resolver

9 years agoUse checkPath when checking IdP
Anders Mörtberg [Thu, 19 Mar 2015 07:58:26 +0000 (08:58 +0100)]
Use checkPath when checking IdP

9 years agoAdd .gitignore
Anders Mörtberg [Thu, 19 Mar 2015 07:58:05 +0000 (08:58 +0100)]
Add .gitignore

9 years agoNames are now strings
Anders Mörtberg [Thu, 19 Mar 2015 07:15:30 +0000 (08:15 +0100)]
Names are now strings

9 years agoAdd J
Anders Mörtberg [Thu, 19 Mar 2015 06:36:46 +0000 (07:36 +0100)]
Add J

9 years agoFix a typo in the parser
Anders Mörtberg [Thu, 19 Mar 2015 06:36:29 +0000 (07:36 +0100)]
Fix a typo in the parser

9 years agoadded transport
Simon Huber [Wed, 18 Mar 2015 23:54:52 +0000 (00:54 +0100)]
added transport

9 years agoshow transport like we parse it; whitespace
Simon Huber [Wed, 18 Mar 2015 23:15:57 +0000 (00:15 +0100)]
show transport like we parse it; whitespace

9 years agoadded app of a formula
Simon Huber [Wed, 18 Mar 2015 22:48:11 +0000 (23:48 +0100)]
added app of a formula

9 years agoAdd Id, Path, AppFormula and Trans.
Anders [Wed, 18 Mar 2015 17:20:06 +0000 (18:20 +0100)]
Add Id, Path, AppFormula and Trans.

funExt is working!

9 years agoAdd Connections
Anders [Wed, 18 Mar 2015 10:57:06 +0000 (11:57 +0100)]
Add Connections

9 years agoRename to cubical
Anders [Wed, 18 Mar 2015 10:53:37 +0000 (11:53 +0100)]
Rename to cubical

9 years agoStart adding Id types
Anders [Wed, 18 Mar 2015 10:50:30 +0000 (11:50 +0100)]
Start adding Id types

9 years agoRemove Neutral data type
Anders [Tue, 17 Mar 2015 13:59:45 +0000 (14:59 +0100)]
Remove Neutral data type

9 years agoClean Resolver
Anders Mörtberg [Wed, 18 Mar 2015 09:15:33 +0000 (10:15 +0100)]
Clean Resolver

9 years agoStart working on cubical type theory
Anders [Mon, 16 Mar 2015 16:09:28 +0000 (17:09 +0100)]
Start working on cubical type theory

9 years agoInitial commit
Anders [Thu, 26 Feb 2015 13:35:29 +0000 (14:35 +0100)]
Initial commit

9 years agoInitial commit
mortberg [Thu, 26 Feb 2015 13:27:28 +0000 (14:27 +0100)]
Initial commit