| Mon, 17 Sep 2012 16:57:22 +0200 |
cleaned up internal naming scheme for bnfs
|
file | diff | annotate |
| Sun, 16 Sep 2012 10:33:25 +0200 |
use strip_typeN in bnf_def (instead of repairing strip_type)
|
file | diff | annotate |
| Fri, 14 Sep 2012 12:09:27 +0200 |
renamed "mk_UnN" to "mk_UnIN"
|
file | diff | annotate |
| Wed, 12 Sep 2012 23:06:39 +0200 |
rough and ready induction
|
file | diff | annotate |
| Wed, 12 Sep 2012 17:26:05 +0200 |
set up things for (co)induction sugar
|
file | diff | annotate |
| Tue, 11 Sep 2012 22:31:43 +0200 |
support for sort constraints in new (co)data commands
|
file | diff | annotate |
| Tue, 11 Sep 2012 17:09:39 +0200 |
renamed "BNF_Library" to "BNF_Util"
|
file | diff | annotate |
| Mon, 10 Sep 2012 17:35:53 +0200 |
use balanced sums for constructors (to gracefully handle 100 constructors or more)
|
file | diff | annotate |
| Sun, 09 Sep 2012 10:58:11 +0200 |
open typedefs everywhere in the package
|
file | diff | annotate |
| Sat, 08 Sep 2012 21:04:26 +0200 |
more sugar on codatatypes
|
file | diff | annotate |
| Sat, 08 Sep 2012 21:04:26 +0200 |
define coiterators
|
file | diff | annotate |
| Sat, 08 Sep 2012 21:04:26 +0200 |
correctly curry recursor arguments
|
file | diff | annotate |
| Thu, 06 Sep 2012 11:46:08 +0200 |
tuning
|
file | diff | annotate |
| Thu, 06 Sep 2012 11:34:05 +0200 |
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
|
file | diff | annotate |
| Thu, 06 Sep 2012 02:56:21 +0200 |
construct high-level iterator RHS
|
file | diff | annotate |
| Tue, 04 Sep 2012 13:06:41 +0200 |
more work on sugar + simplify Trueprop + eq idiom everywhere
|
file | diff | annotate |
| Tue, 04 Sep 2012 13:02:32 +0200 |
more work on FP sugar
|
file | diff | annotate |
| Mon, 03 Sep 2012 11:54:21 +0200 |
rearrange dependencies
|
file | diff | annotate |
| Tue, 28 Aug 2012 17:16:00 +0200 |
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
|
file | diff | annotate |