]> matita.cs.unibo.it Git - helm.git/log
helm.git
14 years ago...
Claudio Sacerdoti Coen [Thu, 4 Feb 2010 13:31:41 +0000 (13:31 +0000)]
...

14 years agoAdded count_occurrences.
Andrea Asperti [Thu, 4 Feb 2010 11:23:52 +0000 (11:23 +0000)]
Added count_occurrences.
Type of does_not_occur corrected.

14 years agoBug fixed: goto_top used to reset the status to the first one and then
Andrea Asperti [Thu, 4 Feb 2010 10:32:30 +0000 (10:32 +0000)]
Bug fixed: goto_top used to reset the status to the first one and then
reset_buffer (re-implemented yesterday) used to do the time travel
again. Fixed by getting rid of goto_top.

Note: the old implementation was slightly more efficient since the
initial notation of Matita was not re-loaded every time you go back to
top. In practice, this does not seem to matter.

14 years ago freescale porting
Cosimo Oliboni [Thu, 4 Feb 2010 07:54:26 +0000 (07:54 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Thu, 4 Feb 2010 03:42:47 +0000 (03:42 +0000)]
 freescale porting

14 years ago...
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 23:14:47 +0000 (23:14 +0000)]
...

14 years agoEnd of curryfication of binary_morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 23:10:57 +0000 (23:10 +0000)]
End of curryfication of binary_morphisms.

14 years agoCurryfication of binary_morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:58:49 +0000 (22:58 +0000)]
Curryfication of binary_morphisms.

14 years agoCurryfication of binary setoids.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:46:21 +0000 (22:46 +0000)]
Curryfication of binary setoids.

14 years agoCurryfication of binary morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:03:37 +0000 (22:03 +0000)]
Curryfication of binary morphisms.

14 years agoWork in Progress: Who needs binary_morphisms? Curryfication is your friend.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 20:03:57 +0000 (20:03 +0000)]
Work in Progress: Who needs binary_morphisms? Curryfication is your friend.

But...

 1) the hints are uglier
 2) you really need to apply mk_binary_morphism to prove a curryfied binary
    morphism if you want to remain sane...

Note: with non uniform coercions everywhere we should be able to finally get
a beautiful script. Yet to be done.

14 years agoDisabled debug prints in ndestruct tactic.
Wilmer Ricciotti [Wed, 3 Feb 2010 17:00:36 +0000 (17:00 +0000)]
Disabled debug prints in ndestruct tactic.

14 years agoDebug code commented out.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 17:00:11 +0000 (17:00 +0000)]
Debug code commented out.

14 years agoParts of the status were not re-initialized correctly during a reset.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 16:56:57 +0000 (16:56 +0000)]
Parts of the status were not re-initialized correctly during a reset.
Fixed (and bugs avoided).

14 years agoBad variable name fixed.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 16:00:33 +0000 (16:00 +0000)]
Bad variable name fixed.

14 years agoBug fixed: projection redexes obtained reducing other projection redexes were
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 15:41:02 +0000 (15:41 +0000)]
Bug fixed: projection redexes obtained reducing other projection redexes were
not reduced.

14 years agoNew version using Streicher's K axiom. Should be faster and also work with
Wilmer Ricciotti [Tue, 2 Feb 2010 18:52:12 +0000 (18:52 +0000)]
New version using Streicher's K axiom. Should be faster and also work with
indexed inductive types.

14 years agoAdded Streicher's K axiom.
Wilmer Ricciotti [Tue, 2 Feb 2010 18:50:29 +0000 (18:50 +0000)]
Added Streicher's K axiom.

14 years agoFixed a bug with indexed inductive types which sometimes prevented the
Wilmer Ricciotti [Tue, 2 Feb 2010 13:39:54 +0000 (13:39 +0000)]
Fixed a bug with indexed inductive types which sometimes prevented the
inversion principles from being defined.

14 years ago freescale porting
Cosimo Oliboni [Tue, 2 Feb 2010 08:38:57 +0000 (08:38 +0000)]
 freescale porting

14 years agolists
Andrea Asperti [Tue, 2 Feb 2010 08:33:37 +0000 (08:33 +0000)]
lists

14 years agoBooleans
Andrea Asperti [Tue, 2 Feb 2010 07:47:13 +0000 (07:47 +0000)]
Booleans

14 years agoboolean arithmetics
Andrea Asperti [Tue, 2 Feb 2010 07:46:03 +0000 (07:46 +0000)]
boolean arithmetics

14 years ago freescale porting
Cosimo Oliboni [Tue, 2 Feb 2010 05:08:53 +0000 (05:08 +0000)]
 freescale porting

14 years ago(no commit message)
Cosimo Oliboni [Mon, 1 Feb 2010 12:40:32 +0000 (12:40 +0000)]

14 years agominus
Andrea Asperti [Mon, 1 Feb 2010 07:57:00 +0000 (07:57 +0000)]
minus

14 years agoOn the last goal at maxdepth we stop at the first solution.
Andrea Asperti [Mon, 1 Feb 2010 07:54:35 +0000 (07:54 +0000)]
On the last goal at maxdepth we stop at the first solution.

14 years ago freescale porting
Cosimo Oliboni [Sun, 31 Jan 2010 06:38:45 +0000 (06:38 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Sat, 30 Jan 2010 09:45:32 +0000 (09:45 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Sat, 30 Jan 2010 08:49:34 +0000 (08:49 +0000)]
 freescale porting

14 years agominus in nat.ma
Andrea Asperti [Fri, 29 Jan 2010 10:16:48 +0000 (10:16 +0000)]
minus in nat.ma

14 years agoNuova gestione della width.
Andrea Asperti [Fri, 29 Jan 2010 10:16:03 +0000 (10:16 +0000)]
Nuova gestione della width.

14 years ago freescale porting
Cosimo Oliboni [Fri, 29 Jan 2010 07:48:08 +0000 (07:48 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Thu, 28 Jan 2010 00:42:24 +0000 (00:42 +0000)]
 freescale porting

14 years agole_arith
Andrea Asperti [Wed, 27 Jan 2010 10:29:07 +0000 (10:29 +0000)]
le_arith

14 years agoUnfolded exact letins during proof reconstruction.
Andrea Asperti [Wed, 27 Jan 2010 09:04:31 +0000 (09:04 +0000)]
Unfolded exact letins during proof reconstruction.

14 years agoAdded a parameter no_implicit (default true) to choose between raising
Andrea Asperti [Wed, 27 Jan 2010 08:47:27 +0000 (08:47 +0000)]
Added a parameter no_implicit (default true) to choose between raising
assert false or returning the identity.

14 years ago freescale porting
Cosimo Oliboni [Wed, 27 Jan 2010 06:39:00 +0000 (06:39 +0000)]
 freescale porting

14 years agole_arith
Andrea Asperti [Tue, 26 Jan 2010 09:20:14 +0000 (09:20 +0000)]
le_arith

14 years ago freescale porting
Cosimo Oliboni [Mon, 25 Jan 2010 22:17:28 +0000 (22:17 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Mon, 25 Jan 2010 06:56:56 +0000 (06:56 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Sun, 24 Jan 2010 05:44:00 +0000 (05:44 +0000)]
 freescale porting

14 years ago(no commit message)
Cosimo Oliboni [Sat, 23 Jan 2010 16:16:40 +0000 (16:16 +0000)]

14 years ago(no commit message)
Cosimo Oliboni [Sat, 23 Jan 2010 16:15:28 +0000 (16:15 +0000)]

14 years ago freescale porting
Cosimo Oliboni [Fri, 22 Jan 2010 23:15:47 +0000 (23:15 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Fri, 22 Jan 2010 01:30:42 +0000 (01:30 +0000)]
 freescale porting

14 years ago(no commit message)
Cosimo Oliboni [Thu, 21 Jan 2010 19:39:17 +0000 (19:39 +0000)]

14 years agoEsempio
Andrea Asperti [Thu, 21 Jan 2010 17:32:19 +0000 (17:32 +0000)]
Esempio

14 years ago(no commit message)
Cosimo Oliboni [Thu, 21 Jan 2010 11:49:45 +0000 (11:49 +0000)]

14 years ago freescale porting, work in progress
Cosimo Oliboni [Thu, 21 Jan 2010 02:16:45 +0000 (02:16 +0000)]
 freescale porting, work in progress

14 years agoWe can always use the "covered by emptyset" relation...
Claudio Sacerdoti Coen [Tue, 19 Jan 2010 12:52:53 +0000 (12:52 +0000)]
We can always use the "covered by emptyset" relation...
Closer and closer to Bove-Capretta, but more and more far away from IGFT...

14 years agoMore //.
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:49:58 +0000 (12:49 +0000)]
More //.

14 years agoMore // everywhere.
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:40:38 +0000 (12:40 +0000)]
More // everywhere.

14 years ago// used everywhere!
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:00:31 +0000 (12:00 +0000)]
// used everywhere!

14 years ago// in place of nauto everywhere
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 11:46:06 +0000 (11:46 +0000)]
// in place of nauto everywhere

14 years ago// is now more powerful
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 10:39:40 +0000 (10:39 +0000)]
// is now more powerful

14 years ago// is now more powerful
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 10:34:24 +0000 (10:34 +0000)]
// is now more powerful

14 years agoNew paramod tac.
Andrea Asperti [Mon, 18 Jan 2010 10:04:51 +0000 (10:04 +0000)]
New paramod tac.

14 years agoInvocation of paramod
Andrea Asperti [Mon, 18 Jan 2010 09:59:04 +0000 (09:59 +0000)]
Invocation of paramod

14 years agoparamod_tac exported
Andrea Asperti [Mon, 18 Jan 2010 09:57:43 +0000 (09:57 +0000)]
paramod_tac exported

14 years agoNumber notation for NG
Andrea Asperti [Mon, 18 Jan 2010 09:51:57 +0000 (09:51 +0000)]
Number notation for NG

14 years agoNumber notation for NG
Andrea Asperti [Mon, 18 Jan 2010 09:51:09 +0000 (09:51 +0000)]
Number notation for NG

14 years agoNumber notation for NG.
Andrea Asperti [Mon, 18 Jan 2010 09:50:06 +0000 (09:50 +0000)]
Number notation for NG.

14 years agoKeeping Implicit for refinement (instead of transforming them to Metas:
Andrea Asperti [Mon, 18 Jan 2010 07:25:27 +0000 (07:25 +0000)]
Keeping Implicit for refinement (instead of transforming them to Metas:
context bug).

14 years agoUpdating.
Andrea Asperti [Mon, 18 Jan 2010 07:23:03 +0000 (07:23 +0000)]
Updating.

14 years agoA slightly more complicated example.
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 17:10:07 +0000 (17:10 +0000)]
A slightly more complicated example.

14 years agoFinished!
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 17:06:45 +0000 (17:06 +0000)]
Finished!

14 years agoWe are still equivalent (even if the definition of ncover is obfuscated).
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 16:15:09 +0000 (16:15 +0000)]
We are still equivalent (even if the definition of ncover is obfuscated).

14 years agoUrrah!
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 16:12:43 +0000 (16:12 +0000)]
Urrah!

14 years agoExtending to the nAx set.
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 15:55:29 +0000 (15:55 +0000)]
Extending to the nAx set.

14 years agoSkipfact function (a partial general recursive function) defined by recursion
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 10:46:34 +0000 (10:46 +0000)]
Skipfact function (a partial general recursive function) defined by recursion
over the cover relation of an IGFT.

14 years agoFixed a bug in the discrimination principle: the refiner was not able to
Wilmer Ricciotti [Tue, 12 Jan 2010 12:23:37 +0000 (12:23 +0000)]
Fixed a bug in the discrimination principle: the refiner was not able to
synthesize the return type of the inner match correctly.

14 years agoFinished
Claudio Sacerdoti Coen [Mon, 11 Jan 2010 16:59:40 +0000 (16:59 +0000)]
Finished

14 years ago1. New paramodulation function
Andrea Asperti [Mon, 11 Jan 2010 11:27:54 +0000 (11:27 +0000)]
1. New paramodulation function
2. goal narrowing works both on the current goal both before and after
demodulation

14 years agosaturate cust be called with delta=0
Andrea Asperti [Mon, 11 Jan 2010 11:23:25 +0000 (11:23 +0000)]
saturate cust be called with delta=0

14 years agoAdded is_equation
Andrea Asperti [Mon, 11 Jan 2010 11:21:58 +0000 (11:21 +0000)]
Added is_equation

14 years agoDebugging info
Andrea Asperti [Mon, 11 Jan 2010 11:21:00 +0000 (11:21 +0000)]
Debugging info

14 years agoImproved
Claudio Sacerdoti Coen [Fri, 8 Jan 2010 18:43:54 +0000 (18:43 +0000)]
Improved

14 years agoPartial porting to new syntax.
Claudio Sacerdoti Coen [Fri, 8 Jan 2010 18:36:06 +0000 (18:36 +0000)]
Partial porting to new syntax.

14 years agoSource language path must be appended, not replaced.
Claudio Sacerdoti Coen [Fri, 8 Jan 2010 17:34:30 +0000 (17:34 +0000)]
Source language path must be appended, not replaced.

14 years agoCategorical stuff postponed.
Claudio Sacerdoti Coen [Fri, 8 Jan 2010 15:18:46 +0000 (15:18 +0000)]
Categorical stuff postponed.

14 years agoThe body of constants is a reference, not the actual body!
Andrea Asperti [Fri, 8 Jan 2010 09:29:51 +0000 (09:29 +0000)]
The body of constants is a reference, not the actual body!

14 years agoremoved debugging info
Andrea Asperti [Fri, 8 Jan 2010 08:23:31 +0000 (08:23 +0000)]
removed debugging info

14 years agorebuilding the library
Andrea Asperti [Fri, 8 Jan 2010 08:19:24 +0000 (08:19 +0000)]
rebuilding the library

14 years agorebuilding the library
Andrea Asperti [Fri, 8 Jan 2010 08:18:20 +0000 (08:18 +0000)]
rebuilding the library

14 years agorebuilding the library
Andrea Asperti [Fri, 8 Jan 2010 08:17:37 +0000 (08:17 +0000)]
rebuilding the library

14 years agoapplyS
Andrea Asperti [Fri, 8 Jan 2010 08:12:06 +0000 (08:12 +0000)]
applyS

14 years agorefresh uri
Andrea Asperti [Fri, 8 Jan 2010 08:11:14 +0000 (08:11 +0000)]
refresh uri
applyS

14 years agoSupport for the new auto tactics //
Andrea Asperti [Fri, 8 Jan 2010 08:10:20 +0000 (08:10 +0000)]
Support for the new auto tactics //

14 years agoSupport for the new // tactics.
Andrea Asperti [Fri, 8 Jan 2010 08:09:39 +0000 (08:09 +0000)]
Support for the new // tactics.

14 years agonew reloc_subst (to avoid cyclic substitutions).
Andrea Asperti [Fri, 8 Jan 2010 08:08:44 +0000 (08:08 +0000)]
new reloc_subst (to avoid cyclic substitutions).
Changed default sig.

14 years ago....
Enrico Tassi [Thu, 7 Jan 2010 23:24:52 +0000 (23:24 +0000)]
....

14 years ago...
Enrico Tassi [Thu, 7 Jan 2010 23:23:09 +0000 (23:23 +0000)]
...

14 years ago...
Enrico Tassi [Thu, 7 Jan 2010 22:53:47 +0000 (22:53 +0000)]
...

14 years agoSimplified.
Claudio Sacerdoti Coen [Wed, 6 Jan 2010 23:03:47 +0000 (23:03 +0000)]
Simplified.

Note: it breaks the file later (maybe a coercion conflict, I suppose).

14 years agoCoercions via unification hints?
Claudio Sacerdoti Coen [Wed, 6 Jan 2010 22:37:10 +0000 (22:37 +0000)]
Coercions via unification hints?

14 years ago- we now add the kernel options in the preamble of the URI hierarchy
Ferruccio Guidi [Tue, 5 Jan 2010 19:13:40 +0000 (19:13 +0000)]
- we now add the kernel options in the preamble of the URI hierarchy
- we now quote the identifiers by default to make them NMTOKENS but we added a command line option to disable this quoting (it can be time consuming)

14 years ago1) stuff moved from categories.ma to setoids*.ma
Claudio Sacerdoti Coen [Sat, 2 Jan 2010 19:40:58 +0000 (19:40 +0000)]
1) stuff moved from categories.ma to setoids*.ma
2) we are now ready to define the category of o-algebras

14 years ago...
Enrico Tassi [Wed, 30 Dec 2009 18:17:43 +0000 (18:17 +0000)]
...

14 years agoAlmost done (up to definition of category).
Claudio Sacerdoti Coen [Wed, 30 Dec 2009 17:41:59 +0000 (17:41 +0000)]
Almost done (up to definition of category).