]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years ago- Added new output in standard C.
Claudio Sacerdoti Coen [Tue, 13 Jan 2009 10:50:29 +0000 (10:50 +0000)]
- Added new output in standard C.

15 years agoSome work on o-algebras towards the proof that a and j are saturation/reduction
Claudio Sacerdoti Coen [Mon, 12 Jan 2009 23:49:29 +0000 (23:49 +0000)]
Some work on o-algebras towards the proof that a and j are saturation/reduction
operators.

15 years agoThe new coercion from SET to Type0 with higher priority really helps a lot:
Claudio Sacerdoti Coen [Thu, 8 Jan 2009 18:47:38 +0000 (18:47 +0000)]
The new coercion from SET to Type0 with higher priority really helps a lot:
almost all explicit occurrences of carr have been removed.

15 years agomore composites to make all happy!
Enrico Tassi [Thu, 8 Jan 2009 18:12:28 +0000 (18:12 +0000)]
more composites to make all happy!

15 years agoeq over SET1 and SET no longer used
Enrico Tassi [Thu, 8 Jan 2009 16:48:36 +0000 (16:48 +0000)]
eq over SET1 and SET no longer used

15 years agosome more if/fi conversion due to the new . binding
Enrico Tassi [Thu, 8 Jan 2009 12:05:34 +0000 (12:05 +0000)]
some more if/fi conversion due to the new . binding

15 years agounary_morphism_N : seoidN -> setoidN -> setoidN (was ... -> setoidN+1)
Enrico Tassi [Thu, 8 Jan 2009 11:57:57 +0000 (11:57 +0000)]
unary_morphism_N : seoidN -> setoidN -> setoidN (was ... -> setoidN+1)
notation for . is now bound to fi instead of if (i.e. rewrites -> )

15 years agovirtuals for () removed and bound to 'o'
Enrico Tassi [Thu, 8 Jan 2009 09:47:46 +0000 (09:47 +0000)]
virtuals for () removed and bound to 'o'
memory changed, used similar symbols are presented first but not altering their original order

15 years agoJust a snapshot.
Claudio Sacerdoti Coen [Thu, 8 Jan 2009 09:08:09 +0000 (09:08 +0000)]
Just a snapshot.

15 years agocoercions reordering implemented
Enrico Tassi [Tue, 6 Jan 2009 18:19:28 +0000 (18:19 +0000)]
coercions reordering implemented

15 years agoupdated
Enrico Tassi [Tue, 6 Jan 2009 18:16:45 +0000 (18:16 +0000)]
updated

15 years agoMore work on concrete spaces.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 17:44:05 +0000 (17:44 +0000)]
More work on concrete spaces.

15 years agoSome work on concrete spaces.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 17:28:59 +0000 (17:28 +0000)]
Some work on concrete spaces.

15 years agoCool: only 8 universes in use.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 16:41:01 +0000 (16:41 +0000)]
Cool: only 8 universes in use.

15 years ago1) Some reorganization.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 16:20:00 +0000 (16:20 +0000)]
1) Some reorganization.
2) Funny: the proof that basic_topologies are an example of o_basic_topology
   is immediate.

15 years agoSome renaming to avoid confusion between saturations and o_saturations.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 15:16:49 +0000 (15:16 +0000)]
Some renaming to avoid confusion between saturations and o_saturations.

15 years agoFixing universe levels for saturations and (partially) basic_topologies.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 15:06:31 +0000 (15:06 +0000)]
Fixing universe levels for saturations and (partially) basic_topologies.

15 years agoThe functor from BP to OBP has been defined (but no property proved yet).
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 14:10:51 +0000 (14:10 +0000)]
The functor from BP to OBP has been defined (but no property proved yet).

15 years agoOk, even if not stated formally, now we know that the map from REL to OA is
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 13:58:06 +0000 (13:58 +0000)]
Ok, even if not stated formally, now we know that the map from REL to OA is
a functor!

15 years agoorelation_of_relation preserves equality and identities.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 13:13:23 +0000 (13:13 +0000)]
orelation_of_relation preserves equality and identities.

15 years agoBasic pairs restored; require renaming to use them together with o-basic_pairs.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 02:05:57 +0000 (02:05 +0000)]
Basic pairs restored; require renaming to use them together with o-basic_pairs.

15 years agoSome progress: everything works well now.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 01:50:28 +0000 (01:50 +0000)]
Some progress: everything works well now.

15 years agoOoops, I forgot to commit this in the previous 3-4 commits.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 01:40:28 +0000 (01:40 +0000)]
Ooops, I forgot to commit this in the previous 3-4 commits.

15 years agoAn hint moved to the right place.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 01:39:36 +0000 (01:39 +0000)]
An hint moved to the right place.

15 years agoNo more daemons, no more exTs.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 01:31:21 +0000 (01:31 +0000)]
No more daemons, no more exTs.

15 years agoGreat: some significant progress in fixing universe levels.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 01:10:01 +0000 (01:10 +0000)]
Great: some significant progress in fixing universe levels.

15 years agoremoving (only from the interface) functions related to ligatures that now live in...
Enrico Tassi [Mon, 5 Jan 2009 16:07:48 +0000 (16:07 +0000)]
removing (only from the interface) functions related to ligatures that now live in the GUI

15 years agoadded help on virtuals and UTF-8 equivalence classes
Enrico Tassi [Mon, 5 Jan 2009 16:07:15 +0000 (16:07 +0000)]
added help on virtuals and UTF-8 equivalence classes

15 years agoexpand ligatures after \n too
Enrico Tassi [Mon, 5 Jan 2009 16:06:53 +0000 (16:06 +0000)]
expand ligatures after \n too

15 years agoadded := -> \def
Enrico Tassi [Mon, 5 Jan 2009 15:33:42 +0000 (15:33 +0000)]
added := -> \def

15 years agoadded some memory to virtuals eq classes
Enrico Tassi [Mon, 5 Jan 2009 15:25:04 +0000 (15:25 +0000)]
added some memory to virtuals eq classes

15 years ago...
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 20:42:32 +0000 (20:42 +0000)]
...

15 years ago1. CProp_n fixed to be equal to Type_n to better understand what is happening
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

15 years agoSnapshot to try to understand something.
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 17:55:20 +0000 (17:55 +0000)]
Snapshot to try to understand something.

15 years agoSome more progress, fighting universe inconsistencies.
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 16:45:36 +0000 (16:45 +0000)]
Some more progress, fighting universe inconsistencies.

15 years agoYet another universe problem :-(
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 15:36:21 +0000 (15:36 +0000)]
Yet another universe problem :-(

15 years ago...
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 13:08:16 +0000 (13:08 +0000)]
...

15 years agoBack to step 1: all files that used to pass now pass again.
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.

15 years agoMore re-organization.
Claudio Sacerdoti Coen [Sun, 4 Jan 2009 10:30:12 +0000 (10:30 +0000)]
More re-organization.

15 years agoBasic pairs went through with no problems.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 18:49:03 +0000 (18:49 +0000)]
Basic pairs went through with no problems.

15 years agoUniverse level fixed (litterally).
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 18:30:01 +0000 (18:30 +0000)]
Universe level fixed (litterally).

15 years agoNiceness was just a temporary illusion :-(
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 18:27:07 +0000 (18:27 +0000)]
Niceness was just a temporary illusion :-(

15 years agoMuch, much nicer now.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 18:03:33 +0000 (18:03 +0000)]
Much, much nicer now.

15 years agoSome more re-organization.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 17:48:52 +0000 (17:48 +0000)]
Some more re-organization.

15 years agoMore re-working.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 16:41:15 +0000 (16:41 +0000)]
More re-working.

15 years agoMore reorganization.
Claudio Sacerdoti Coen [Sat, 3 Jan 2009 16:16:09 +0000 (16:16 +0000)]
More reorganization.

15 years agoequivalence_relations made uniform w.r.t. universe level
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.

15 years agoFinal work for today.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 18:20:31 +0000 (18:20 +0000)]
Final work for today.

15 years agoremoved duplicate notation
Enrico Tassi [Sun, 28 Dec 2008 18:06:59 +0000 (18:06 +0000)]
removed duplicate notation

15 years agoSome more painful work.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 17:47:25 +0000 (17:47 +0000)]
Some more painful work.

15 years agobinary_meet is back again, with some effort
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 17:23:10 +0000 (17:23 +0000)]
binary_meet is back again, with some effort

15 years agoMany universe inconsistency avoided here and there.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 16:52:37 +0000 (16:52 +0000)]
Many universe inconsistency avoided here and there.

15 years agoThe universe inconsistency comes from big union, that uses the existential.
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.

15 years agoProof that \Omega \sup A is an overlap algebra, up to universe inconsistency :-(
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 :-(

15 years agoo-algebra defined again
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 15:14:43 +0000 (15:14 +0000)]
o-algebra defined again

15 years agoCategories and subsets compile again, hopefully with better universe levels.
Claudio Sacerdoti Coen [Sun, 28 Dec 2008 14:32:18 +0000 (14:32 +0000)]
Categories and subsets compile again, hopefully with better universe levels.

15 years agoWARNING: partial commit to try to understand something.
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.

15 years agoSome more fixes. Boring and stupid!
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 18:31:27 +0000 (18:31 +0000)]
Some more fixes. Boring and stupid!

15 years agoSome fixes.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 18:12:47 +0000 (18:12 +0000)]
Some fixes.

15 years agoO-Basic Topologies do form a category.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 17:56:15 +0000 (17:56 +0000)]
O-Basic Topologies do form a category.

15 years agoA few more lines.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 17:19:51 +0000 (17:19 +0000)]
A few more lines.

15 years agoSome notes by Giovanni.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 17:17:47 +0000 (17:17 +0000)]
Some notes by Giovanni.

15 years agoSome notes by Giovanni.
Claudio Sacerdoti Coen [Fri, 26 Dec 2008 17:17:19 +0000 (17:17 +0000)]
Some notes by Giovanni.

15 years agoadded some virtuals
Enrico Tassi [Wed, 24 Dec 2008 16:17:11 +0000 (16:17 +0000)]
added some virtuals

15 years agobug fixed, all convertible was called without a metasenv
Enrico Tassi [Wed, 24 Dec 2008 15:31:20 +0000 (15:31 +0000)]
bug fixed, all convertible was called without a metasenv

15 years agoJust copied here from formal_topologies.ma.
Claudio Sacerdoti Coen [Mon, 22 Dec 2008 22:36:20 +0000 (22:36 +0000)]
Just copied here from formal_topologies.ma.

15 years agoMore (ugly) work.
Claudio Sacerdoti Coen [Mon, 22 Dec 2008 22:32:55 +0000 (22:32 +0000)]
More (ugly) work.

15 years ago...
Enrico Tassi [Mon, 22 Dec 2008 21:08:46 +0000 (21:08 +0000)]
...

15 years agoBeginning of o-basic_topologies.
Enrico Tassi [Mon, 22 Dec 2008 18:07:58 +0000 (18:07 +0000)]
Beginning of o-basic_topologies.

15 years agoSome clean up.
Enrico Tassi [Mon, 22 Dec 2008 18:07:42 +0000 (18:07 +0000)]
Some clean up.

15 years agoConcrete Spaces defined but... they require about 20m to type-check!
Enrico Tassi [Mon, 22 Dec 2008 17:28:50 +0000 (17:28 +0000)]
Concrete Spaces defined but... they require about 20m to type-check!

15 years ago1 more lemma
Enrico Tassi [Mon, 22 Dec 2008 16:45:59 +0000 (16:45 +0000)]
1 more lemma

15 years agoone line
Enrico Tassi [Mon, 22 Dec 2008 15:22:44 +0000 (15:22 +0000)]
one line

15 years agosome work
Enrico Tassi [Mon, 22 Dec 2008 14:25:53 +0000 (14:25 +0000)]
some work

15 years agoums got rid of
Claudio Sacerdoti Coen [Mon, 22 Dec 2008 00:02:01 +0000 (00:02 +0000)]
ums got rid of

15 years ago1) no more DAEMONS
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

15 years agomerged commits, the same proof is missing :-(
Enrico Tassi [Sun, 21 Dec 2008 21:58:47 +0000 (21:58 +0000)]
merged commits, the same proof is missing :-(

15 years agobleah
Enrico Tassi [Sun, 21 Dec 2008 21:47:57 +0000 (21:47 +0000)]
bleah

15 years agoUsing the new category SET.
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.

15 years agoNew category SET (whose objects are setoids).
Claudio Sacerdoti Coen [Sun, 21 Dec 2008 17:56:31 +0000 (17:56 +0000)]
New category SET (whose objects are setoids).

15 years agowe started the support for naive sort inclusion
Ferruccio Guidi [Sat, 20 Dec 2008 15:27:24 +0000 (15:27 +0000)]
we started the support for naive sort inclusion

15 years agobetter pp of virtuals
Enrico Tassi [Fri, 19 Dec 2008 21:45:45 +0000 (21:45 +0000)]
better pp of virtuals

15 years ago...
Enrico Tassi [Fri, 19 Dec 2008 21:32:18 +0000 (21:32 +0000)]
...

15 years agomore pps
Enrico Tassi [Fri, 19 Dec 2008 20:38:13 +0000 (20:38 +0000)]
more pps

15 years agotype3
Enrico Tassi [Fri, 19 Dec 2008 20:37:50 +0000 (20:37 +0000)]
type3

15 years agoranking hopefully fixed
Enrico Tassi [Fri, 19 Dec 2008 20:37:27 +0000 (20:37 +0000)]
ranking hopefully fixed

15 years ago...
Enrico Tassi [Fri, 19 Dec 2008 20:37:07 +0000 (20:37 +0000)]
...

15 years agofix exponentiation
Enrico Tassi [Fri, 19 Dec 2008 20:20:15 +0000 (20:20 +0000)]
fix exponentiation

15 years agogo notation go!
Enrico Tassi [Fri, 19 Dec 2008 16:23:15 +0000 (16:23 +0000)]
go notation go!

15 years agofixed, it seems the new handling of hints in some rare cases made inference stupid
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

15 years ago...
Enrico Tassi [Fri, 19 Dec 2008 10:57:37 +0000 (10:57 +0000)]
...

15 years ago...
Enrico Tassi [Fri, 19 Dec 2008 10:40:51 +0000 (10:40 +0000)]
...

15 years ago...
Enrico Tassi [Fri, 19 Dec 2008 10:37:20 +0000 (10:37 +0000)]
...

15 years agoadded aliases for _ and fixed greek leters thanks to wilmer
Enrico Tassi [Fri, 19 Dec 2008 10:36:00 +0000 (10:36 +0000)]
added aliases for _ and fixed greek leters thanks to wilmer

15 years agobetter pps
Enrico Tassi [Fri, 19 Dec 2008 10:12:15 +0000 (10:12 +0000)]
better pps

15 years agohandles bad Appl
Enrico Tassi [Fri, 19 Dec 2008 10:11:39 +0000 (10:11 +0000)]
handles bad Appl

15 years agoadded better debug_pps and add_user_provided_unification_hint
Enrico Tassi [Fri, 19 Dec 2008 10:11:14 +0000 (10:11 +0000)]
added better debug_pps and add_user_provided_unification_hint

15 years ago...
Enrico Tassi [Fri, 19 Dec 2008 10:10:18 +0000 (10:10 +0000)]
...

15 years agoadded unification hint
Enrico Tassi [Fri, 19 Dec 2008 10:09:53 +0000 (10:09 +0000)]
added unification hint

15 years agounification hint
Enrico Tassi [Fri, 19 Dec 2008 10:07:15 +0000 (10:07 +0000)]
unification hint