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

15 years agoSome changes to the pullback test, for debugging
Wilmer Ricciotti [Mon, 15 Dec 2008 19:20:08 +0000 (19:20 +0000)]
Some changes to the pullback test, for debugging

15 years agoFirst attempt to implement unification hints.
Wilmer Ricciotti [Mon, 15 Dec 2008 19:16:46 +0000 (19:16 +0000)]
First attempt to implement unification hints.

15 years agouse named types to force some constraints asap
Enrico Tassi [Mon, 15 Dec 2008 13:50:17 +0000 (13:50 +0000)]
use named types to force some constraints asap

15 years agoTo check if a term is type, do a whd of its sort before matching it.
Enrico Tassi [Mon, 15 Dec 2008 13:26:26 +0000 (13:26 +0000)]
To check if a term is type, do a whd of its sort before matching it.

15 years ago...
Enrico Tassi [Mon, 15 Dec 2008 13:13:33 +0000 (13:13 +0000)]
...

15 years agoaded some whd, you should be able to declare something like:
Enrico Tassi [Mon, 15 Dec 2008 13:12:28 +0000 (13:12 +0000)]
aded some whd, you should be able to declare something like:
 inductive A : FOO :=
where FOO is defined as a sort (or unfolds to somthing ending with a sort)

15 years agoThe library is no longer automatically used during disambiguation.
Claudio Sacerdoti Coen [Sun, 14 Dec 2008 23:03:02 +0000 (23:03 +0000)]
The library is no longer automatically used during disambiguation.
It is used only when the user press the More button or when he selects
the library from the Debug (?????) menu!

Moreover, using the library or not using it has now a different behaviour:
1. when the library is NOT used, symbols with no preferences are no
   longer automatically looked for in the library
2. when the library IS used, only passes 5 and 6 are tried.

CONS:
1. the Debug menu voice is now necessary: move it elsewhere? always open the
   disambiguation window making it non-modal? put an hyperlink in the error
   message window?
2. when the library is used, all previous preferences are completely ignored
   for all symbols. This makes the system much more stupid than what it used
   to be.

PROS:
disambiguation is now much faster in case of error

15 years ago- improved logging
Ferruccio Guidi [Sun, 14 Dec 2008 22:22:38 +0000 (22:22 +0000)]
- improved logging
- optimization in subst

15 years agonew kernel basic_ag (with absolute local references)
Ferruccio Guidi [Sun, 14 Dec 2008 19:34:19 +0000 (19:34 +0000)]
new kernel basic_ag (with absolute local references)

15 years agowe are changing the kernel version from basic_rg to basic_ag
Ferruccio Guidi [Sun, 14 Dec 2008 15:32:38 +0000 (15:32 +0000)]
we are changing the kernel version from basic_rg to basic_ag

15 years agoautItem : the uris of the objects involved in the implicit coercions
Ferruccio Guidi [Sun, 14 Dec 2008 15:23:54 +0000 (15:23 +0000)]
autItem : the uris of the objects involved in the implicit coercions
log     : improved log output
basic_rg: improved logging

15 years ago...
Enrico Tassi [Sun, 14 Dec 2008 11:37:50 +0000 (11:37 +0000)]
...

15 years agoeureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg fd => c ] is
Enrico Tassi [Sun, 14 Dec 2008 11:36:02 +0000 (11:36 +0000)]
eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg fd => c ] is
now correctly broken if too long

15 years ago...
Enrico Tassi [Sun, 14 Dec 2008 10:56:38 +0000 (10:56 +0000)]
...

15 years agoimproved type hierarchy management
Ferruccio Guidi [Fri, 12 Dec 2008 21:26:57 +0000 (21:26 +0000)]
improved type hierarchy management

15 years ago...
Claudio Sacerdoti Coen [Fri, 12 Dec 2008 14:59:39 +0000 (14:59 +0000)]
...

15 years agoA parser (and a scanner) to import "~C" files into Matita.
Claudio Sacerdoti Coen [Fri, 12 Dec 2008 14:41:18 +0000 (14:41 +0000)]
A parser (and a scanner) to import "~C" files into Matita.

15 years ago...
Claudio Sacerdoti Coen [Fri, 12 Dec 2008 14:32:56 +0000 (14:32 +0000)]
...

15 years ago1. new expressions AND, OR, XOR
Claudio Sacerdoti Coen [Fri, 12 Dec 2008 14:32:23 +0000 (14:32 +0000)]
1. new expressions AND, OR, XOR
2. constants must be initialized
3. bug fixed: the size n of an array means that the array
   has (n+1) elements. Thus the last valid index is n.

15 years ago- basic_rg: architectural bug fix
Ferruccio Guidi [Fri, 12 Dec 2008 12:45:42 +0000 (12:45 +0000)]
- basic_rg: architectural bug fix
- toplevel: more help on command line options

15 years ago...
Enrico Tassi [Fri, 12 Dec 2008 12:14:31 +0000 (12:14 +0000)]
...

15 years agoadded some hardcoded universes, needed to typecheck the librarya
Enrico Tassi [Fri, 12 Dec 2008 12:11:54 +0000 (12:11 +0000)]
added some hardcoded universes, needed to typecheck the librarya

15 years agoadded some messages
Enrico Tassi [Fri, 12 Dec 2008 12:11:12 +0000 (12:11 +0000)]
added some messages

15 years agoadded empty_db, usefull to avoid translating all old coercions to obtain a new coerci...
Enrico Tassi [Fri, 12 Dec 2008 12:10:40 +0000 (12:10 +0000)]
added empty_db, usefull to avoid translating all old coercions to obtain a new coercions database