]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agocomponents/library: dotdothack removed
Ferruccio Guidi [Tue, 4 Mar 2008 19:10:48 +0000 (19:10 +0000)]
components/library: dotdothack removed
legacy & LAMBDA-TYPES support $(MATITAUSEROPTIONS) (= -system for fguidi)
LAMBDA-TYPES: two missing generation lemmas added

16 years agoNew syntax for patterns.
Claudio Sacerdoti Coen [Tue, 4 Mar 2008 16:42:17 +0000 (16:42 +0000)]
New syntax for patterns.

16 years agoprodT ==> prod
Claudio Sacerdoti Coen [Tue, 4 Mar 2008 16:12:25 +0000 (16:12 +0000)]
prodT ==> prod

16 years agoA) New version.
Claudio Sacerdoti Coen [Tue, 4 Mar 2008 15:44:36 +0000 (15:44 +0000)]
A) New version.
B) set "baseuri" removed
C) minor clean-up

16 years agowe added the classic substitution function
Ferruccio Guidi [Fri, 29 Feb 2008 18:13:10 +0000 (18:13 +0000)]
we added the classic substitution function

16 years agofirs attempt to compile with ocamlbuild
Enrico Tassi [Thu, 28 Feb 2008 08:42:37 +0000 (08:42 +0000)]
firs attempt to compile with ocamlbuild

16 years agothe proof of bertrand's conjecture is now complete
Wilmer Ricciotti [Wed, 27 Feb 2008 17:03:01 +0000 (17:03 +0000)]
the proof of bertrand's conjecture is now complete

16 years agoI added some debugging information
Ferruccio Guidi [Tue, 26 Feb 2008 17:23:37 +0000 (17:23 +0000)]
I added some debugging information

16 years agoadded MATITAOPTIONS -onepass as for LAMBDA-TYPES
Ferruccio Guidi [Tue, 26 Feb 2008 17:20:47 +0000 (17:20 +0000)]
added MATITAOPTIONS -onepass as for LAMBDA-TYPES

16 years agoLAMBDA-TYPES: added wf3 (legal context predicate);
Ferruccio Guidi [Tue, 26 Feb 2008 17:16:12 +0000 (17:16 +0000)]
LAMBDA-TYPES: added wf3 (legal context predicate);
              Unified-Sub removed because of its early stage

16 years ago$(H) added :)
Ferruccio Guidi [Sun, 24 Feb 2008 19:29:44 +0000 (19:29 +0000)]
$(H) added :)

16 years agoLAMBDA-TYPES: dependences calculation improved
Ferruccio Guidi [Sun, 24 Feb 2008 19:22:40 +0000 (19:22 +0000)]
LAMBDA-TYPES: dependences calculation improved

16 years agoLAMBDA-TYPES:
Ferruccio Guidi [Sat, 23 Feb 2008 21:58:11 +0000 (21:58 +0000)]
LAMBDA-TYPES:
we introduced incremental dependences build to speed up the compilation
dependences are now dynamic so the file "depends" was removed from svn

16 years ago- added some options to matitadep: -stdout and -exclude
Ferruccio Guidi [Fri, 22 Feb 2008 22:25:27 +0000 (22:25 +0000)]
- added some options to matitadep: -stdout and -exclude
- LAMBDA-TYPES: improved Makefile, Base-2/theory.mma is no longer needed

16 years agosieve of erathostene (proof of soundness almost done)
Wilmer Ricciotti [Fri, 22 Feb 2008 17:34:56 +0000 (17:34 +0000)]
sieve of erathostene (proof of soundness almost done)

16 years agoA new very simple example for recursive functions. Still bugged, but getting
Claudio Sacerdoti Coen [Thu, 21 Feb 2008 19:03:09 +0000 (19:03 +0000)]
A new very simple example for recursive functions. Still bugged, but getting
better.

16 years agoAvoid translating back recursive fixes to the same URI.
Claudio Sacerdoti Coen [Thu, 21 Feb 2008 19:02:04 +0000 (19:02 +0000)]
Avoid translating back recursive fixes to the same URI.

16 years agoAvoid application to 0 arguments.
Claudio Sacerdoti Coen [Thu, 21 Feb 2008 18:57:28 +0000 (18:57 +0000)]
Avoid application to 0 arguments.

16 years agoBetter handling of exceptions.
Claudio Sacerdoti Coen [Thu, 21 Feb 2008 18:56:44 +0000 (18:56 +0000)]
Better handling of exceptions.

16 years agosvn:ignores fixed
Ferruccio Guidi [Thu, 21 Feb 2008 15:32:50 +0000 (15:32 +0000)]
svn:ignores fixed

16 years ago-onepass option removed from Makefile to comile Base-2/ext/arith.ma ???
Ferruccio Guidi [Wed, 20 Feb 2008 19:30:11 +0000 (19:30 +0000)]
-onepass option removed from Makefile to comile Base-2/ext/arith.ma ???

16 years agoLambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
Ferruccio Guidi [Wed, 20 Feb 2008 18:53:47 +0000 (18:53 +0000)]
LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
some additions and redundant dependences fixed

16 years agosplat_args is now better understood and debugged: we need TWO splat_args, one when
Enrico Tassi [Wed, 20 Feb 2008 17:48:16 +0000 (17:48 +0000)]
splat_args is now better understood and debugged: we need TWO splat_args, one when
the term is a Rel (that skips the bound variables) and one when the term is a Fix
(that passes bound variables around).

16 years agoadded small test, fixed some bugs
Enrico Tassi [Wed, 20 Feb 2008 16:53:59 +0000 (16:53 +0000)]
added small test, fixed some bugs

16 years agomany fixed in translation functions
Enrico Tassi [Wed, 20 Feb 2008 14:49:22 +0000 (14:49 +0000)]
many fixed in translation functions

16 years agodependences needed a fix :)
Ferruccio Guidi [Tue, 19 Feb 2008 19:24:14 +0000 (19:24 +0000)]
dependences needed a fix :)

16 years agowe are moving the devel root one dir level up
Ferruccio Guidi [Tue, 19 Feb 2008 17:16:12 +0000 (17:16 +0000)]
we are moving the devel root one dir level up

16 years ago...
Enrico Tassi [Tue, 19 Feb 2008 17:05:43 +0000 (17:05 +0000)]
...

16 years agosnapshot inverse tranformation
Enrico Tassi [Tue, 19 Feb 2008 16:55:40 +0000 (16:55 +0000)]
snapshot inverse tranformation

16 years agotransformation almost finisced, not tested
Enrico Tassi [Tue, 19 Feb 2008 15:38:00 +0000 (15:38 +0000)]
transformation almost finisced, not tested

16 years agonow inline "file.ma" is allowed.
Ferruccio Guidi [Tue, 19 Feb 2008 13:00:29 +0000 (13:00 +0000)]
now inline "file.ma" is allowed.
file.ma must be compiled and all its contents are inlined

16 years agoAdded o.ma (some results about the magnitude of functions *)
Andrea Asperti [Tue, 19 Feb 2008 12:27:10 +0000 (12:27 +0000)]
Added o.ma (some results about the magnitude of functions *)

16 years agoinitial steps of convertibility
Enrico Tassi [Tue, 19 Feb 2008 11:13:39 +0000 (11:13 +0000)]
initial steps of convertibility

16 years agosome bits of reduction, reusing psubst
Enrico Tassi [Mon, 18 Feb 2008 16:31:32 +0000 (16:31 +0000)]
some bits of reduction, reusing psubst

16 years agoComplete proof of Bertrand for n >= 256.
Andrea Asperti [Mon, 18 Feb 2008 08:56:40 +0000 (08:56 +0000)]
Complete proof of Bertrand for n >= 256.
Removed the baseuri form all files in nat.

16 years agoPrima versione di bertrand. Tanti cambiamenti qua e la.
Andrea Asperti [Thu, 14 Feb 2008 15:41:46 +0000 (15:41 +0000)]
Prima versione di bertrand. Tanti cambiamenti qua e la.

16 years agobaseuris removed from files
Ferruccio Guidi [Wed, 13 Feb 2008 17:56:43 +0000 (17:56 +0000)]
baseuris removed from files

16 years agofixed dependences
Ferruccio Guidi [Wed, 13 Feb 2008 17:24:39 +0000 (17:24 +0000)]
fixed dependences

16 years agoconversion half inplemented
Enrico Tassi [Wed, 13 Feb 2008 17:18:25 +0000 (17:18 +0000)]
conversion half inplemented

16 years agorenaming
Ferruccio Guidi [Wed, 13 Feb 2008 17:15:06 +0000 (17:15 +0000)]
renaming

16 years agoreordered cases
Enrico Tassi [Wed, 13 Feb 2008 16:00:16 +0000 (16:00 +0000)]
reordered cases

16 years agoreorganization of sources
Enrico Tassi [Wed, 13 Feb 2008 15:42:28 +0000 (15:42 +0000)]
reorganization of sources

16 years agosubstituion and lifting implemented
Enrico Tassi [Wed, 13 Feb 2008 15:35:43 +0000 (15:35 +0000)]
substituion and lifting implemented

16 years agorenaming
Ferruccio Guidi [Wed, 13 Feb 2008 13:40:54 +0000 (13:40 +0000)]
renaming

16 years agofactorized common components of objects
Enrico Tassi [Wed, 13 Feb 2008 13:17:38 +0000 (13:17 +0000)]
factorized common components of objects

16 years agoadded Local pragma, moved leftno and inductive into obj, added relevance attribute...
Enrico Tassi [Wed, 13 Feb 2008 13:01:15 +0000 (13:01 +0000)]
added Local pragma, moved leftno and inductive into obj, added relevance attribute of parameters

16 years agoadded leftno to indtypes, better indentation and comments
Enrico Tassi [Wed, 13 Feb 2008 12:46:12 +0000 (12:46 +0000)]
added leftno to indtypes, better indentation and comments

16 years agonCic almost finished
Enrico Tassi [Tue, 12 Feb 2008 18:02:14 +0000 (18:02 +0000)]
nCic almost finished

16 years agorenaming
Ferruccio Guidi [Tue, 12 Feb 2008 16:21:19 +0000 (16:21 +0000)]
renaming

16 years agoregeneration with new results
Ferruccio Guidi [Tue, 12 Feb 2008 16:02:28 +0000 (16:02 +0000)]
regeneration with new results

16 years agofixed path for matitadep
Enrico Tassi [Tue, 12 Feb 2008 12:09:41 +0000 (12:09 +0000)]
fixed path for matitadep

16 years agofixed make dist
Enrico Tassi [Tue, 12 Feb 2008 12:09:20 +0000 (12:09 +0000)]
fixed make dist

16 years agobetter error message in case inclusion failed
Enrico Tassi [Tue, 12 Feb 2008 12:08:39 +0000 (12:08 +0000)]
better error message in case inclusion failed

16 years agoallow to use "../foo/bar.ma" as a path for the include statement
Enrico Tassi [Tue, 12 Feb 2008 12:06:26 +0000 (12:06 +0000)]
allow to use "../foo/bar.ma" as a path for the include statement

16 years agoprogress.
Andrea Asperti [Fri, 8 Feb 2008 17:04:43 +0000 (17:04 +0000)]
progress.

16 years agoA formalization of modified realisability with truth as in
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 15:22:32 +0000 (15:22 +0000)]
A formalization of modified realisability with truth as in
``Internalising modified realisability in constructive type theory'',
Erik Palmgren, Logical Methods in Computer Science, Vol 1. (2:2), 2005, pp 1--7.

16 years agoBug fixed in generation of elimination principles of inductive types having
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 13:44:54 +0000 (13:44 +0000)]
Bug fixed in generation of elimination principles of inductive types having
at least one constructor of type (A -> i) -> i that was not the last
constructor.

16 years agoprodT merged with prod
Claudio Sacerdoti Coen [Fri, 8 Feb 2008 11:50:42 +0000 (11:50 +0000)]
prodT merged with prod
fstT merged with fst
sndT merged with fst

16 years agoProdT was a perfect copy of Prod. Removed.
Claudio Sacerdoti Coen [Thu, 7 Feb 2008 18:08:50 +0000 (18:08 +0000)]
ProdT was a perfect copy of Prod. Removed.
Sum is now in Type.

16 years agoResults about Chebyshev teta function.
Andrea Asperti [Thu, 7 Feb 2008 12:02:01 +0000 (12:02 +0000)]
Results about Chebyshev teta function.

16 years agocic defined (half)
Enrico Tassi [Tue, 5 Feb 2008 17:45:38 +0000 (17:45 +0000)]
cic defined (half)

16 years agoSome more theorems.
Andrea Asperti [Tue, 5 Feb 2008 16:21:37 +0000 (16:21 +0000)]
Some more theorems.

16 years agoreindent
Enrico Tassi [Tue, 5 Feb 2008 16:12:33 +0000 (16:12 +0000)]
reindent

16 years agooldenv2newenv cache
Enrico Tassi [Tue, 5 Feb 2008 16:06:20 +0000 (16:06 +0000)]
oldenv2newenv cache

16 years agouri and references(uri)
Enrico Tassi [Tue, 5 Feb 2008 15:54:52 +0000 (15:54 +0000)]
uri and references(uri)

16 years agouri -> reference (2)
Enrico Tassi [Tue, 5 Feb 2008 15:23:08 +0000 (15:23 +0000)]
uri -> reference (2)

16 years agouri -> reference
Enrico Tassi [Tue, 5 Feb 2008 15:20:38 +0000 (15:20 +0000)]
uri -> reference

16 years agolower bound for neper's constant
Wilmer Ricciotti [Tue, 5 Feb 2008 15:10:20 +0000 (15:10 +0000)]
lower bound for neper's constant

16 years agosad snapshot
Enrico Tassi [Mon, 4 Feb 2008 15:13:59 +0000 (15:13 +0000)]
sad snapshot

16 years agosnapshot
Enrico Tassi [Mon, 4 Feb 2008 11:00:54 +0000 (11:00 +0000)]
snapshot

16 years agosnapshot
Enrico Tassi [Mon, 4 Feb 2008 10:57:45 +0000 (10:57 +0000)]
snapshot

16 years agoImproved approximations for A and prim.
Andrea Asperti [Mon, 4 Feb 2008 08:55:10 +0000 (08:55 +0000)]
Improved approximations for A and prim.

16 years agoSome improvement.
Andrea Asperti [Mon, 4 Feb 2008 08:39:17 +0000 (08:39 +0000)]
Some improvement.

16 years agovery bad bug found, asert false in cicReduction when a clear is performed
Enrico Tassi [Fri, 1 Feb 2008 09:29:09 +0000 (09:29 +0000)]
very bad bug found, asert false in cicReduction when a clear is performed

16 years agoOne Obj.magic implemented, trust changed to false.
Wilmer Ricciotti [Thu, 31 Jan 2008 16:30:40 +0000 (16:30 +0000)]
One Obj.magic implemented, trust changed to false.

16 years agoTransformation back and forth between old and new representation
Wilmer Ricciotti [Thu, 31 Jan 2008 16:20:46 +0000 (16:20 +0000)]
Transformation back and forth between old and new representation

16 years agosnapshot
Enrico Tassi [Thu, 31 Jan 2008 15:27:47 +0000 (15:27 +0000)]
snapshot

16 years agonew uri defined
Enrico Tassi [Thu, 31 Jan 2008 15:06:31 +0000 (15:06 +0000)]
new uri defined

16 years agoSquare root added.
Wilmer Ricciotti [Thu, 31 Jan 2008 14:51:45 +0000 (14:51 +0000)]
Square root added.

16 years agosnapshot]
Enrico Tassi [Thu, 31 Jan 2008 14:50:19 +0000 (14:50 +0000)]
snapshot]

16 years agosnapshot
Enrico Tassi [Thu, 31 Jan 2008 12:43:37 +0000 (12:43 +0000)]
snapshot

16 years agoadded meta for the new kernel
Enrico Tassi [Wed, 30 Jan 2008 16:29:04 +0000 (16:29 +0000)]
added meta for the new kernel

16 years agostub functions to make all compile
Enrico Tassi [Wed, 30 Jan 2008 16:26:06 +0000 (16:26 +0000)]
stub functions to make all compile

16 years agobasic organization of the new kernel
Enrico Tassi [Wed, 30 Jan 2008 10:42:22 +0000 (10:42 +0000)]
basic organization of the new kernel

16 years agoImproved approximations
Andrea Asperti [Wed, 30 Jan 2008 09:13:06 +0000 (09:13 +0000)]
Improved approximations

16 years agoNew approximtions.
Andrea Asperti [Tue, 29 Jan 2008 10:57:02 +0000 (10:57 +0000)]
New approximtions.

16 years ago...
Enrico Tassi [Thu, 24 Jan 2008 10:37:11 +0000 (10:37 +0000)]
...

16 years agosnapshot with more duality, almost where we left without duality
Enrico Tassi [Wed, 23 Jan 2008 12:44:39 +0000 (12:44 +0000)]
snapshot with more duality, almost where we left without duality

16 years ago...
Enrico Tassi [Tue, 22 Jan 2008 17:54:05 +0000 (17:54 +0000)]
...

16 years agoBertrand's conjecture (weak), some work in progress
Wilmer Ricciotti [Tue, 22 Jan 2008 10:41:43 +0000 (10:41 +0000)]
Bertrand's conjecture (weak), some work in progress

16 years agosnapshot
Enrico Tassi [Mon, 21 Jan 2008 18:05:11 +0000 (18:05 +0000)]
snapshot

16 years agoMatitac now accepts multiple targets :-) (but only in the same root :-(
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:35:11 +0000 (17:35 +0000)]
Matitac now accepts multiple targets :-) (but only in the same root :-(

16 years agoHack for code extraction re-linked, but disactivated.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:30:35 +0000 (17:30 +0000)]
Hack for code extraction re-linked, but disactivated.

16 years agoOld tiny freescale experiment get rid of.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:29:48 +0000 (17:29 +0000)]
Old tiny freescale experiment get rid of.
New shiny freescale formalization by Cosimo Oliboni <oliboni@cs.unibo.it>,
described in his Laurea Thesis.

16 years agoTypo fixed.
Claudio Sacerdoti Coen [Mon, 21 Jan 2008 17:18:32 +0000 (17:18 +0000)]
Typo fixed.

16 years agosnopshot before isabellization
Enrico Tassi [Mon, 21 Jan 2008 11:21:36 +0000 (11:21 +0000)]
snopshot before isabellization

16 years agosnapshot
Enrico Tassi [Wed, 16 Jan 2008 15:48:53 +0000 (15:48 +0000)]
snapshot

16 years ago3.27 ok
Enrico Tassi [Wed, 16 Jan 2008 13:32:05 +0000 (13:32 +0000)]
3.27 ok

16 years agoyes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!
Enrico Tassi [Wed, 16 Jan 2008 12:04:06 +0000 (12:04 +0000)]
yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!

16 years agoupdate: upper bound for prim
Wilmer Ricciotti [Tue, 15 Jan 2008 14:38:50 +0000 (14:38 +0000)]
update: upper bound for prim