]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

15 years agolambda case fixed, used to not properly use the expected type if it was not a Prod
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

15 years agoadded 'unification hint command to add a term to the new unification hint database'
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'

15 years agoidentity coercions are not really inserted, just used as hints for unification
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

15 years ago....
Enrico Tassi [Fri, 19 Dec 2008 09:59:54 +0000 (09:59 +0000)]
....

15 years agoStupid bug fixed: checkin the type in place of the sort during the refinement
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.

15 years agoNew disambiguation commented out.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:41:30 +0000 (20:41 +0000)]
New disambiguation commented out.

15 years agoMany axioms are now proved... using many more (but simpler) axioms.
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.

15 years agoNow it compiles again.
Claudio Sacerdoti Coen [Thu, 18 Dec 2008 20:32:15 +0000 (20:32 +0000)]
Now it compiles again.

15 years agoRefinement of axioms fixed. We did not check that the declared type must be
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.

15 years ago- improved logging
Ferruccio Guidi [Thu, 18 Dec 2008 15:48:01 +0000 (15:48 +0000)]
- improved logging
- we started to support the coercion for "non"

15 years ago...
Enrico Tassi [Thu, 18 Dec 2008 13:56:15 +0000 (13:56 +0000)]
...

15 years agowe started the support for the coercions "alle" and "alli"
Ferruccio Guidi [Wed, 17 Dec 2008 19:49:35 +0000 (19:49 +0000)]
we started the support for the coercions "alle" and "alli"

15 years agofoo overlap
Enrico Tassi [Wed, 17 Dec 2008 17:52:18 +0000 (17:52 +0000)]
foo overlap

15 years agofoo overlap
Enrico Tassi [Wed, 17 Dec 2008 17:35:00 +0000 (17:35 +0000)]
foo overlap

15 years ago....
Enrico Tassi [Wed, 17 Dec 2008 15:20:44 +0000 (15:20 +0000)]
....

15 years agowe added the implicit coercion for modus tollens
Ferruccio Guidi [Tue, 16 Dec 2008 19:32:12 +0000 (19:32 +0000)]
we added the implicit coercion for modus tollens

15 years agoprevious change was causing divergence
Enrico Tassi [Tue, 16 Dec 2008 19:14:01 +0000 (19:14 +0000)]
previous change was causing divergence

15 years agohints work better now
Enrico Tassi [Tue, 16 Dec 2008 19:13:46 +0000 (19:13 +0000)]
hints work better now

15 years agohints attached
Enrico Tassi [Tue, 16 Dec 2008 13:58:09 +0000 (13:58 +0000)]
hints attached

15 years agoremoved debug code
Enrico Tassi [Tue, 16 Dec 2008 13:57:22 +0000 (13:57 +0000)]
removed debug code

15 years agofixed a bug, it used to report o wrong is_normal bit in case of match
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

15 years agomake it compile again
Enrico Tassi [Tue, 16 Dec 2008 13:53:16 +0000 (13:53 +0000)]
make it compile again

15 years agowrap object_not_found
Enrico Tassi [Tue, 16 Dec 2008 13:53:03 +0000 (13:53 +0000)]
wrap object_not_found

15 years agomove the printing in the right place
Enrico Tassi [Tue, 16 Dec 2008 13:50:55 +0000 (13:50 +0000)]
move the printing in the right place

15 years agoauto expansion of \tex macros added as a switch in the edit menu
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

15 years agoadded one asser
Enrico Tassi [Tue, 16 Dec 2008 09:00:17 +0000 (09:00 +0000)]
added one asser

15 years agodep.opt regenerated
Enrico Tassi [Mon, 15 Dec 2008 22:55:17 +0000 (22:55 +0000)]
dep.opt regenerated

15 years agoadded unification hints
Enrico Tassi [Mon, 15 Dec 2008 22:49:47 +0000 (22:49 +0000)]
added unification hints