cubicaltt.git
9 years agoif A and B are isomorphic, prop A -> prop B, normal form
coquand [Sun, 19 Apr 2015 13:47:19 +0000 (15:47 +0200)]
if A and B are isomorphic, prop A -> prop B, normal form

9 years agoresult on equivalence of fibers
coquand [Sun, 19 Apr 2015 10:12:08 +0000 (12:12 +0200)]
result on equivalence of fibers

9 years agonew proof of Hedberg's theorem
coquand [Sun, 19 Apr 2015 10:09:20 +0000 (12:09 +0200)]
new proof of Hedberg's theorem

9 years agoFix printing of goals and environments (TODO: Fix "susp (bool)"...)
Anders [Fri, 17 Apr 2015 15:18:04 +0000 (17:18 +0200)]
Fix printing of goals and environments (TODO: Fix "susp (bool)"...)

9 years agoRewrite app and support using case-of
Anders [Fri, 17 Apr 2015 14:20:13 +0000 (16:20 +0200)]
Rewrite app and support using case-of

9 years agoUse Except instead or Error
Anders [Fri, 17 Apr 2015 12:38:07 +0000 (14:38 +0200)]
Use Except instead or Error

9 years agoRemove tabs
Anders [Fri, 17 Apr 2015 12:37:39 +0000 (14:37 +0200)]
Remove tabs

9 years agoOnly show second part of VPi x (VLam ...)
Anders Mörtberg [Fri, 17 Apr 2015 08:50:01 +0000 (10:50 +0200)]
Only show second part of VPi x (VLam ...)

9 years agoAlso normalize the type of lambdas and print VPi nicer
Anders Mörtberg [Fri, 17 Apr 2015 08:35:30 +0000 (10:35 +0200)]
Also normalize the type of lambdas and print VPi nicer

9 years agoUse showTer1 to print closures
Anders Mörtberg [Fri, 17 Apr 2015 07:13:23 +0000 (09:13 +0200)]
Use showTer1 to print closures

9 years agoFix uafunext2
Anders Mörtberg [Fri, 17 Apr 2015 07:13:09 +0000 (09:13 +0200)]
Fix uafunext2

9 years agoRemove some incidentally commited holes
Anders [Thu, 16 Apr 2015 15:18:59 +0000 (17:18 +0200)]
Remove some incidentally commited holes

9 years agoReintroduce _ in identifier again
Anders [Thu, 16 Apr 2015 13:22:53 +0000 (15:22 +0200)]
Reintroduce _ in identifier again

9 years agoreintroduce nicer mkVar
Simon Huber [Thu, 16 Apr 2015 13:15:58 +0000 (15:15 +0200)]
reintroduce nicer mkVar

9 years agokeep name if we have it when generating a fresh name
Simon Huber [Thu, 16 Apr 2015 12:49:14 +0000 (14:49 +0200)]
keep name if we have it when generating a fresh name

9 years agochange mkVar back to how it was
Simon Huber [Thu, 16 Apr 2015 12:32:17 +0000 (14:32 +0200)]
change mkVar back to how it was

9 years agoAdd indentation to Checking and start changing mkVar (not working as expected wrt...
Anders Mörtberg [Thu, 16 Apr 2015 09:18:09 +0000 (11:18 +0200)]
Add indentation to Checking and start changing mkVar (not working as expected wrt holes)

9 years agoOnly print File loaded if file type checks
Anders Mörtberg [Thu, 16 Apr 2015 09:17:30 +0000 (11:17 +0200)]
Only print File loaded if file type checks

9 years agoChange gensym
Anders Mörtberg [Thu, 16 Apr 2015 09:17:12 +0000 (11:17 +0200)]
Change gensym

9 years agoMake holes print the context
Anders Mörtberg [Thu, 16 Apr 2015 09:16:03 +0000 (11:16 +0200)]
Make holes print the context

9 years agoTrailing whitespace
Anders Mörtberg [Thu, 16 Apr 2015 09:13:58 +0000 (11:13 +0200)]
Trailing whitespace

9 years agoFix undefined
Anders Mörtberg [Thu, 16 Apr 2015 09:13:38 +0000 (11:13 +0200)]
Fix undefined

9 years agoFinish example of integers as a HIT
Anders [Wed, 15 Apr 2015 09:47:38 +0000 (11:47 +0200)]
Finish example of integers as a HIT

9 years agoRemove some code from ex1
Anders [Wed, 15 Apr 2015 09:47:20 +0000 (11:47 +0200)]
Remove some code from ex1

9 years agoFix bug in type checker for HITs
Anders [Wed, 15 Apr 2015 09:47:06 +0000 (11:47 +0200)]
Fix bug in type checker for HITs

9 years agoFix undefined
Anders [Wed, 15 Apr 2015 09:46:54 +0000 (11:46 +0200)]
Fix undefined

9 years agoRemove VUndef
Anders Mörtberg [Wed, 15 Apr 2015 08:30:43 +0000 (10:30 +0200)]
Remove VUndef

9 years agoAdd very simple support for holes
Anders Mörtberg [Wed, 15 Apr 2015 08:14:27 +0000 (10:14 +0200)]
Add very simple support for holes

9 years agoMake list compile
Anders Mörtberg [Tue, 14 Apr 2015 21:04:00 +0000 (23:04 +0200)]
Make list compile

9 years agoMake undefined only occur as a declaration so that the type can be inferred
Anders Mörtberg [Tue, 14 Apr 2015 21:03:53 +0000 (23:03 +0200)]
Make undefined only occur as a declaration so that the type can be inferred

9 years agoUndef is neutral (but there is an issue with inferType for undef)
Anders Mörtberg [Tue, 14 Apr 2015 20:20:17 +0000 (22:20 +0200)]
Undef is neutral (but there is an issue with inferType for undef)

9 years agoStart defining integers as a HIT and proving that they are a set
Anders Mörtberg [Tue, 14 Apr 2015 20:19:49 +0000 (22:19 +0200)]
Start defining integers as a HIT and proving that they are a set

9 years agoFix printing of fst, snd and lambdas
Anders [Tue, 14 Apr 2015 14:55:04 +0000 (16:55 +0200)]
Fix printing of fst, snd and lambdas

9 years agoUpdate the description in demo.ctt
Anders [Tue, 14 Apr 2015 14:54:50 +0000 (16:54 +0200)]
Update the description in demo.ctt

9 years agoadded some lines in ex1.ctt
coquand [Tue, 14 Apr 2015 11:31:43 +0000 (13:31 +0200)]
added some lines in ex1.ctt

9 years agoadded some lines in ex1.ctt
coquand [Tue, 14 Apr 2015 11:30:18 +0000 (13:30 +0200)]
added some lines in ex1.ctt

9 years agosmall change in helix.ctt
coquand [Tue, 14 Apr 2015 06:53:44 +0000 (08:53 +0200)]
small change in helix.ctt

9 years agoone example with constant functions
coquand [Tue, 14 Apr 2015 06:19:50 +0000 (08:19 +0200)]
one example with constant functions

9 years agoFix bug in Resolver
Anders Mörtberg [Mon, 13 Apr 2015 21:33:52 +0000 (23:33 +0200)]
Fix bug in Resolver

9 years agoRemove contr from equiv
Anders Mörtberg [Mon, 13 Apr 2015 21:06:14 +0000 (23:06 +0200)]
Remove contr from equiv

9 years agolicense should include names
Simon Huber [Mon, 13 Apr 2015 19:17:51 +0000 (21:17 +0200)]
license should include names

9 years agosmall modification in the file susp
coquand [Mon, 13 Apr 2015 18:19:32 +0000 (20:19 +0200)]
small modification in the file susp

9 years agoUpdate help message
Anders Mörtberg [Mon, 13 Apr 2015 17:41:32 +0000 (19:41 +0200)]
Update help message

9 years agoUpdate README
Anders Mörtberg [Mon, 13 Apr 2015 17:41:25 +0000 (19:41 +0200)]
Update README

9 years agoMove stream to experiments
Anders Mörtberg [Mon, 13 Apr 2015 17:41:17 +0000 (19:41 +0200)]
Move stream to experiments

9 years agoAdd dependency graph script
Anders [Mon, 13 Apr 2015 15:01:30 +0000 (17:01 +0200)]
Add dependency graph script

9 years agoUpdate README
Anders [Mon, 13 Apr 2015 15:01:13 +0000 (17:01 +0200)]
Update README

9 years agoLots of cleaning in the examples
Anders [Mon, 13 Apr 2015 14:39:28 +0000 (16:39 +0200)]
Lots of cleaning in the examples

9 years agoAdd equiv and uafunext2
Anders [Mon, 13 Apr 2015 13:54:12 +0000 (15:54 +0200)]
Add equiv and uafunext2

9 years agoReorganized and cleaned some examples
Anders [Mon, 13 Apr 2015 13:53:07 +0000 (15:53 +0200)]
Reorganized and cleaned some examples

9 years agoUpdate README
Anders [Mon, 13 Apr 2015 13:18:15 +0000 (15:18 +0200)]
Update README

9 years agoFix README
Anders [Mon, 13 Apr 2015 13:03:42 +0000 (15:03 +0200)]
Fix README

9 years agoUpdate README
Anders [Mon, 13 Apr 2015 13:01:59 +0000 (15:01 +0200)]
Update README

9 years agoUpdate the README and examples
Anders [Mon, 13 Apr 2015 12:55:24 +0000 (14:55 +0200)]
Update the README and examples

9 years agodemo from the proglog talk
Simon Huber [Mon, 13 Apr 2015 12:44:39 +0000 (14:44 +0200)]
demo from the proglog talk

9 years agouse smart fst/snd in act
Simon Huber [Mon, 13 Apr 2015 09:36:20 +0000 (11:36 +0200)]
use smart fst/snd in act

9 years agoadded thierrys examples (funext from univalence,helix)
Simon Huber [Sun, 12 Apr 2015 08:37:17 +0000 (10:37 +0200)]
added thierrys examples (funext from univalence,helix)

9 years agofixing use of isNeutral
Simon Huber [Sat, 11 Apr 2015 17:11:36 +0000 (19:11 +0200)]
fixing use of isNeutral

9 years agoFix parsing of trans, comp, etc.
Anders [Fri, 10 Apr 2015 13:41:24 +0000 (15:41 +0200)]
Fix parsing of trans, comp, etc.

9 years agoExplicitly pass around the history
Anders [Fri, 10 Apr 2015 12:45:33 +0000 (14:45 +0200)]
Explicitly pass around the history

9 years agoMerge pull request #6 from nad/master
mortberg [Fri, 10 Apr 2015 08:28:33 +0000 (10:28 +0200)]
Merge pull request #6 from nad/master

Proved (?) that equality coincides with bisimilarity.

9 years agoStart the proof that ua implies funext
Anders Mörtberg [Thu, 9 Apr 2015 20:58:11 +0000 (22:58 +0200)]
Start the proof that ua implies funext

9 years agoProved (?) that equality coincides with bisimilarity.
Nils Anders Danielsson [Thu, 9 Apr 2015 14:35:00 +0000 (16:35 +0200)]
Proved (?) that equality coincides with bisimilarity.

With help from Thierry Coquand and Simon Huber.

9 years agoClean examples
Anders [Thu, 9 Apr 2015 12:29:27 +0000 (14:29 +0200)]
Clean examples

9 years agoAdd normalization function
Anders [Thu, 9 Apr 2015 12:29:01 +0000 (14:29 +0200)]
Add normalization function

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