]>
matita.cs.unibo.it Git - helm.git/log
Enrico Tassi [Mon, 5 Jan 2009 16:06:53 +0000 (16:06 +0000)]
expand ligatures after \n too
Enrico Tassi [Mon, 5 Jan 2009 15:33:42 +0000 (15:33 +0000)]
added := -> \def
Enrico Tassi [Mon, 5 Jan 2009 15:25:04 +0000 (15:25 +0000)]
added some memory to virtuals eq classes
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 20:42:32 +0000 (20:42 +0000)]
...
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 20:33:56 +0000 (20:33 +0000)]
1. CProp_n fixed to be equal to Type_n to better understand what is happening
with universe levels
2. major proof step: I have proved (up to universe inconsistency :-( that
every RELation induces an OA morphism. In particular, these means:
A) having correctly defined the four images on subsets
B) having proved the fundamental symmetry
C) having proved the two fundamental adjunctions
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 17:55:20 +0000 (17:55 +0000)]
Snapshot to try to understand something.
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 16:45:36 +0000 (16:45 +0000)]
Some more progress, fighting universe inconsistencies.
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 15:36:21 +0000 (15:36 +0000)]
Yet another universe problem :-(
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 13:08:16 +0000 (13:08 +0000)]
...
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 13:01:49 +0000 (13:01 +0000)]
Back to step 1: all files that used to pass now pass again.
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 10:30:12 +0000 (10:30 +0000)]
More re-organization.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 18:49:03 +0000 (18:49 +0000)]
Basic pairs went through with no problems.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 18:30:01 +0000 (18:30 +0000)]
Universe level fixed (litterally).
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 18:27:07 +0000 (18:27 +0000)]
Niceness was just a temporary illusion :-(
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 18:03:33 +0000 (18:03 +0000)]
Much, much nicer now.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 17:48:52 +0000 (17:48 +0000)]
Some more re-organization.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 16:41:15 +0000 (16:41 +0000)]
More re-working.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 16:16:09 +0000 (16:16 +0000)]
More reorganization.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 19:49:23 +0000 (19:49 +0000)]
equivalence_relations made uniform w.r.t. universe level
However, there is still a bug related to universes, which I do not understand.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 18:20:31 +0000 (18:20 +0000)]
Final work for today.
Enrico Tassi [Sun, 28 Dec 2008 18:06:59 +0000 (18:06 +0000)]
removed duplicate notation
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 17:47:25 +0000 (17:47 +0000)]
Some more painful work.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 17:23:10 +0000 (17:23 +0000)]
binary_meet is back again, with some effort
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 16:52:37 +0000 (16:52 +0000)]
Many universe inconsistency avoided here and there.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 16:28:58 +0000 (16:28 +0000)]
The universe inconsistency comes from big union, that uses the existential.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 16:10:34 +0000 (16:10 +0000)]
Proof that \Omega \sup A is an overlap algebra, up to universe inconsistency :-(
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 15:14:43 +0000 (15:14 +0000)]
o-algebra defined again
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 14:32:18 +0000 (14:32 +0000)]
Categories and subsets compile again, hopefully with better universe levels.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 12:42:21 +0000 (12:42 +0000)]
WARNING: partial commit to try to understand something.
I have fixed the universes in categories, adding a new category (of level 2)
and trying to prove that powersets form a SET1.
Failing, so far.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 18:31:27 +0000 (18:31 +0000)]
Some more fixes. Boring and stupid!
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 18:12:47 +0000 (18:12 +0000)]
Some fixes.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 17:56:15 +0000 (17:56 +0000)]
O-Basic Topologies do form a category.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 17:19:51 +0000 (17:19 +0000)]
A few more lines.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 17:17:47 +0000 (17:17 +0000)]
Some notes by Giovanni.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 17:17:19 +0000 (17:17 +0000)]
Some notes by Giovanni.
Enrico Tassi [Wed, 24 Dec 2008 16:17:11 +0000 (16:17 +0000)]
added some virtuals
Enrico Tassi [Wed, 24 Dec 2008 15:31:20 +0000 (15:31 +0000)]
bug fixed, all convertible was called without a metasenv
Claudio Sacerdoti Coen [Mon, 22 Dec 2008 22:36:20 +0000 (22:36 +0000)]
Just copied here from formal_topologies.ma.
Claudio Sacerdoti Coen [Mon, 22 Dec 2008 22:32:55 +0000 (22:32 +0000)]
More (ugly) work.
Enrico Tassi [Mon, 22 Dec 2008 21:08:46 +0000 (21:08 +0000)]
...
Enrico Tassi [Mon, 22 Dec 2008 18:07:58 +0000 (18:07 +0000)]
Beginning of o-basic_topologies.
Enrico Tassi [Mon, 22 Dec 2008 18:07:42 +0000 (18:07 +0000)]
Some clean up.
Enrico Tassi [Mon, 22 Dec 2008 17:28:50 +0000 (17:28 +0000)]
Concrete Spaces defined but... they require about 20m to type-check!
Enrico Tassi [Mon, 22 Dec 2008 16:45:59 +0000 (16:45 +0000)]
1 more lemma
Enrico Tassi [Mon, 22 Dec 2008 15:22:44 +0000 (15:22 +0000)]
one line
Enrico Tassi [Mon, 22 Dec 2008 14:25:53 +0000 (14:25 +0000)]
some work
Claudio Sacerdoti Coen [Mon, 22 Dec 2008 00:02:01 +0000 (00:02 +0000)]
ums got rid of
Claudio Sacerdoti Coen [Sun, 21 Dec 2008 23:56:30 +0000 (23:56 +0000)]
1) no more DAEMONS
2) f, f-, f*, f-* are morphisms now
Enrico Tassi [Sun, 21 Dec 2008 21:58:47 +0000 (21:58 +0000)]
merged commits, the same proof is missing :-(
Enrico Tassi [Sun, 21 Dec 2008 21:47:57 +0000 (21:47 +0000)]
bleah
Claudio Sacerdoti Coen [Sun, 21 Dec 2008 21:46:04 +0000 (21:46 +0000)]
Using the new category SET.
Rewriting is no longer working as expected.
Claudio Sacerdoti Coen [Sun, 21 Dec 2008 17:56:31 +0000 (17:56 +0000)]
New category SET (whose objects are setoids).
Ferruccio Guidi [Sat, 20 Dec 2008 15:27:24 +0000 (15:27 +0000)]
we started the support for naive sort inclusion
Enrico Tassi [Fri, 19 Dec 2008 21:45:45 +0000 (21:45 +0000)]
better pp of virtuals
Enrico Tassi [Fri, 19 Dec 2008 21:32:18 +0000 (21:32 +0000)]
...
Enrico Tassi [Fri, 19 Dec 2008 20:38:13 +0000 (20:38 +0000)]
more pps
Enrico Tassi [Fri, 19 Dec 2008 20:37:50 +0000 (20:37 +0000)]
type3
Enrico Tassi [Fri, 19 Dec 2008 20:37:27 +0000 (20:37 +0000)]
ranking hopefully fixed
Enrico Tassi [Fri, 19 Dec 2008 20:37:07 +0000 (20:37 +0000)]
...
Enrico Tassi [Fri, 19 Dec 2008 20:20:15 +0000 (20:20 +0000)]
fix exponentiation
Enrico Tassi [Fri, 19 Dec 2008 16:23:15 +0000 (16:23 +0000)]
go notation go!
Enrico Tassi [Fri, 19 Dec 2008 12:44:13 +0000 (12:44 +0000)]
fixed, it seems the new handling of hints in some rare cases made inference stupid
Enrico Tassi [Fri, 19 Dec 2008 10:57:37 +0000 (10:57 +0000)]
...
Enrico Tassi [Fri, 19 Dec 2008 10:40:51 +0000 (10:40 +0000)]
...
Enrico Tassi [Fri, 19 Dec 2008 10:37:20 +0000 (10:37 +0000)]
...
Enrico Tassi [Fri, 19 Dec 2008 10:36:00 +0000 (10:36 +0000)]
added aliases for _ and fixed greek leters thanks to wilmer
Enrico Tassi [Fri, 19 Dec 2008 10:12:15 +0000 (10:12 +0000)]
better pps
Enrico Tassi [Fri, 19 Dec 2008 10:11:39 +0000 (10:11 +0000)]
handles bad Appl
Enrico Tassi [Fri, 19 Dec 2008 10:11:14 +0000 (10:11 +0000)]
added better debug_pps and add_user_provided_unification_hint
Enrico Tassi [Fri, 19 Dec 2008 10:10:18 +0000 (10:10 +0000)]
...
Enrico Tassi [Fri, 19 Dec 2008 10:09:53 +0000 (10:09 +0000)]
added unification hint
Enrico Tassi [Fri, 19 Dec 2008 10:07:15 +0000 (10:07 +0000)]
unification hint
Enrico Tassi [Fri, 19 Dec 2008 10:06:31 +0000 (10:06 +0000)]
lambda case fixed, used to not properly use the expected type if it was not a Prod
Enrico Tassi [Fri, 19 Dec 2008 10:05:31 +0000 (10:05 +0000)]
added 'unification hint command to add a term to the new unification hint database'
Enrico Tassi [Fri, 19 Dec 2008 10:02:11 +0000 (10:02 +0000)]
identity coercions are not really inserted, just used as hints for unification
Enrico Tassi [Fri, 19 Dec 2008 09:59:54 +0000 (09:59 +0000)]
....
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:44:31 +0000 (20:44 +0000)]
Stupid bug fixed: checkin the type in place of the sort during the refinement
of axioms.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:41:30 +0000 (20:41 +0000)]
New disambiguation commented out.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:35:07 +0000 (20:35 +0000)]
Many axioms are now proved... using many more (but simpler) axioms.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:32:15 +0000 (20:32 +0000)]
Now it compiles again.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:29:33 +0000 (20:29 +0000)]
Refinement of axioms fixed. We did not check that the declared type must be
a type.
Ferruccio Guidi [Thu, 18 Dec 2008 15:48:01 +0000 (15:48 +0000)]
- improved logging
- we started to support the coercion for "non"
Enrico Tassi [Thu, 18 Dec 2008 13:56:15 +0000 (13:56 +0000)]
...
Ferruccio Guidi [Wed, 17 Dec 2008 19:49:35 +0000 (19:49 +0000)]
we started the support for the coercions "alle" and "alli"
Enrico Tassi [Wed, 17 Dec 2008 17:52:18 +0000 (17:52 +0000)]
foo overlap
Enrico Tassi [Wed, 17 Dec 2008 17:35:00 +0000 (17:35 +0000)]
foo overlap
Enrico Tassi [Wed, 17 Dec 2008 15:20:44 +0000 (15:20 +0000)]
....
Ferruccio Guidi [Tue, 16 Dec 2008 19:32:12 +0000 (19:32 +0000)]
we added the implicit coercion for modus tollens
Enrico Tassi [Tue, 16 Dec 2008 19:14:01 +0000 (19:14 +0000)]
previous change was causing divergence
Enrico Tassi [Tue, 16 Dec 2008 19:13:46 +0000 (19:13 +0000)]
hints work better now
Enrico Tassi [Tue, 16 Dec 2008 13:58:09 +0000 (13:58 +0000)]
hints attached
Enrico Tassi [Tue, 16 Dec 2008 13:57:22 +0000 (13:57 +0000)]
removed debug code
Enrico Tassi [Tue, 16 Dec 2008 13:54:37 +0000 (13:54 +0000)]
fixed a bug, it used to report o wrong is_normal bit in case of match
Enrico Tassi [Tue, 16 Dec 2008 13:53:16 +0000 (13:53 +0000)]
make it compile again
Enrico Tassi [Tue, 16 Dec 2008 13:53:03 +0000 (13:53 +0000)]
wrap object_not_found
Enrico Tassi [Tue, 16 Dec 2008 13:50:55 +0000 (13:50 +0000)]
move the printing in the right place
Enrico Tassi [Tue, 16 Dec 2008 09:00:31 +0000 (09:00 +0000)]
auto expansion of \tex macros added as a switch in the edit menu
Enrico Tassi [Tue, 16 Dec 2008 09:00:17 +0000 (09:00 +0000)]
added one asser
Enrico Tassi [Mon, 15 Dec 2008 22:55:17 +0000 (22:55 +0000)]
dep.opt regenerated
Enrico Tassi [Mon, 15 Dec 2008 22:49:47 +0000 (22:49 +0000)]
added unification hints