]> matita.cs.unibo.it Git - helm.git/log
helm.git
11 years agohigh level semantics
Andrea Asperti [Fri, 18 Jan 2013 11:41:17 +0000 (11:41 +0000)]
high level semantics

11 years agohigh level semantics
Andrea Asperti [Fri, 18 Jan 2013 11:08:33 +0000 (11:08 +0000)]
high level semantics

11 years agosemantics of uni_step
Andrea Asperti [Fri, 18 Jan 2013 10:32:00 +0000 (10:32 +0000)]
semantics of uni_step

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 16:01:27 +0000 (16:01 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 15:54:07 +0000 (15:54 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 15:34:55 +0000 (15:34 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 14:47:22 +0000 (14:47 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 14:05:02 +0000 (14:05 +0000)]
progress

11 years agoMoved a list comparison function in the list file
Andrea Asperti [Thu, 17 Jan 2013 14:00:11 +0000 (14:00 +0000)]
Moved a list comparison function in the list file

11 years agonormal and tuples
Andrea Asperti [Thu, 17 Jan 2013 12:59:25 +0000 (12:59 +0000)]
normal and tuples

11 years ago- paths and left residuals: first case of the equivalence proved!
Ferruccio Guidi [Wed, 16 Jan 2013 19:05:56 +0000 (19:05 +0000)]
- paths and left residuals: first case of the equivalence proved!
- some corrections and additions
- some "?" removed in customized eliminations

11 years agoadded null character to the alphabet
Wilmer Ricciotti [Wed, 16 Jan 2013 16:01:54 +0000 (16:01 +0000)]
added null character to the alphabet

11 years agoprogress
Wilmer Ricciotti [Wed, 16 Jan 2013 11:02:20 +0000 (11:02 +0000)]
progress

11 years ago- some additions and renaming ...
Ferruccio Guidi [Tue, 15 Jan 2013 20:08:08 +0000 (20:08 +0000)]
- some additions and renaming ...

11 years agoprogress in unistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 16:48:30 +0000 (16:48 +0000)]
progress in unistep_aux

11 years agounistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 15:38:57 +0000 (15:38 +0000)]
unistep_aux

11 years agomore unistep
Wilmer Ricciotti [Tue, 15 Jan 2013 15:38:11 +0000 (15:38 +0000)]
more unistep

11 years agounistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 12:29:35 +0000 (12:29 +0000)]
unistep_aux

11 years agocopy finished
Andrea Asperti [Tue, 15 Jan 2013 11:35:33 +0000 (11:35 +0000)]
copy finished

11 years ago- a few more lemmas ...
Ferruccio Guidi [Tue, 15 Jan 2013 10:34:32 +0000 (10:34 +0000)]
- a few more lemmas ...
- some renaming

11 years agocopy.ma
Andrea Asperti [Tue, 15 Jan 2013 09:45:58 +0000 (09:45 +0000)]
copy.ma

11 years agomatch.ma completed
Wilmer Ricciotti [Mon, 14 Jan 2013 16:45:27 +0000 (16:45 +0000)]
match.ma completed

11 years agomatch termination completed, still a small case ignored in wsem_match
Wilmer Ricciotti [Mon, 14 Jan 2013 16:24:17 +0000 (16:24 +0000)]
match termination completed, still a small case ignored in wsem_match

11 years agowsem_match finished
Wilmer Ricciotti [Mon, 14 Jan 2013 15:47:08 +0000 (15:47 +0000)]
wsem_match finished

11 years agoadvancement in match
Wilmer Ricciotti [Mon, 14 Jan 2013 15:14:11 +0000 (15:14 +0000)]
advancement in match

11 years agoClosed some daemons
Andrea Asperti [Mon, 14 Jan 2013 11:46:18 +0000 (11:46 +0000)]
Closed some daemons

11 years agonth_current_chars
Andrea Asperti [Mon, 14 Jan 2013 10:36:34 +0000 (10:36 +0000)]
nth_current_chars

11 years agostandardization: equivalence between paths and left residuals started
Ferruccio Guidi [Sun, 13 Jan 2013 19:10:32 +0000 (19:10 +0000)]
standardization: equivalence between paths and left residuals started

11 years agomatch almost finished
Wilmer Ricciotti [Fri, 11 Jan 2013 23:28:57 +0000 (23:28 +0000)]
match almost finished

11 years agomore porting to machines that can move without writing
Andrea Asperti [Tue, 8 Jan 2013 12:03:01 +0000 (12:03 +0000)]
more porting to machines that can move without writing

11 years agoparmove based on end of the tape
Wilmer Ricciotti [Tue, 8 Jan 2013 10:26:00 +0000 (10:26 +0000)]
parmove based on end of the tape

11 years agoporting to machine that can move without writing
Wilmer Ricciotti [Tue, 8 Jan 2013 09:16:34 +0000 (09:16 +0000)]
porting to machine that can move without writing

11 years agodependences update
Ferruccio Guidi [Sun, 6 Jan 2013 20:09:18 +0000 (20:09 +0000)]
dependences update

11 years agorefactoring ...
Ferruccio Guidi [Sun, 6 Jan 2013 16:17:47 +0000 (16:17 +0000)]
refactoring ...

11 years agoPorted permutation.ma and fermat_little_theorem.ma
Andrea Asperti [Sat, 5 Jan 2013 16:22:16 +0000 (16:22 +0000)]
Ported permutation.ma and fermat_little_theorem.ma

11 years agorefactoring
Andrea Asperti [Thu, 3 Jan 2013 16:49:01 +0000 (16:49 +0000)]
refactoring

11 years agoRefactoring
Andrea Asperti [Thu, 3 Jan 2013 16:33:59 +0000 (16:33 +0000)]
Refactoring

11 years agoChebishev ported
Andrea Asperti [Thu, 3 Jan 2013 16:15:54 +0000 (16:15 +0000)]
Chebishev ported

11 years agolambda: some refactoring + support for subsets of subterms started
Ferruccio Guidi [Wed, 2 Jan 2013 22:12:53 +0000 (22:12 +0000)]
lambda: some refactoring + support for subsets of subterms started
core_notation: some "term 19" added
predefined_virtuals: an addition

11 years ago- probe: new application to compute some data on the proof objects of
Ferruccio Guidi [Tue, 1 Jan 2013 23:01:20 +0000 (23:01 +0000)]
- probe: new application to compute some data on the proof objects of
a development, such as their net size (aka intrinsinc complexity)
- lambdadelta: Makefile now asks "probe" fore some data

11 years agoupdate in basic_2
Ferruccio Guidi [Sun, 30 Dec 2012 13:11:10 +0000 (13:11 +0000)]
update in basic_2

11 years agocommit completed! some bugs fixed and some instances of auto resized
Ferruccio Guidi [Sun, 30 Dec 2012 13:00:21 +0000 (13:00 +0000)]
commit completed! some bugs fixed and some instances of auto resized

11 years agoxoa: change in naming convenctions for existential quantifies
Ferruccio Guidi [Fri, 28 Dec 2012 16:32:01 +0000 (16:32 +0000)]
xoa: change in naming convenctions for existential quantifies
     to cope with ex2 in lib
lib: some additions
lambdadelta: partial commit in basic_2: just grammar, substitution,
unfold, static

11 years ago- lambda_delta: programmed renaming to lambdadelta
Ferruccio Guidi [Tue, 25 Dec 2012 21:48:14 +0000 (21:48 +0000)]
- lambda_delta: programmed renaming to lambdadelta
- nat: general weight-based eliminator added for lambdadelta

11 years ago- we introduced the pointer_step rc in the perspective of proving
Ferruccio Guidi [Sun, 23 Dec 2012 15:02:32 +0000 (15:02 +0000)]
- we introduced the pointer_step rc in the perspective of proving
results on head normal forms
- some renaming

11 years agosome renaming ...
Ferruccio Guidi [Fri, 21 Dec 2012 18:12:41 +0000 (18:12 +0000)]
some renaming ...

11 years agoone file was missing .... :(
Ferruccio Guidi [Fri, 21 Dec 2012 18:06:10 +0000 (18:06 +0000)]
one file was missing .... :(

11 years agoMany changes
Andrea Asperti [Fri, 21 Dec 2012 12:39:18 +0000 (12:39 +0000)]
Many changes

11 years agomem/append lemmas
Andrea Asperti [Fri, 21 Dec 2012 11:13:51 +0000 (11:13 +0000)]
mem/append lemmas

11 years agobertrand OK.
Andrea Asperti [Fri, 21 Dec 2012 11:10:49 +0000 (11:10 +0000)]
bertrand OK.

11 years ago- nat.ma: cut removed from f_ind :)
Ferruccio Guidi [Thu, 20 Dec 2012 14:52:58 +0000 (14:52 +0000)]
- nat.ma: cut removed from f_ind :)
- lanbda: some refactoring

11 years agoreordering and corrections
Ferruccio Guidi [Wed, 19 Dec 2012 20:27:22 +0000 (20:27 +0000)]
reordering and corrections

11 years agobertrand!
Andrea Asperti [Wed, 19 Dec 2012 17:05:03 +0000 (17:05 +0000)]
bertrand!
-tThis line, and those below, will be ignored--

A    chebyshev/bertrand256.ma
A    chebyshev/bertrand.ma

11 years agowe simplified our proof of standardization
Ferruccio Guidi [Wed, 19 Dec 2012 15:52:59 +0000 (15:52 +0000)]
we simplified our proof of standardization
by removing Kashima's "hap" computation

11 years agosqrt.ma
Andrea Asperti [Wed, 19 Dec 2012 07:10:58 +0000 (07:10 +0000)]
sqrt.ma

11 years ago- star.ma: strip lemma and confluence of star
Ferruccio Guidi [Tue, 18 Dec 2012 16:50:35 +0000 (16:50 +0000)]
- star.ma: strip lemma and confluence of star
- lambda: confluence of labelled sequential reduction completed!

11 years agoaddenda
Andrea Asperti [Tue, 18 Dec 2012 13:41:34 +0000 (13:41 +0000)]
addenda

11 years agochanges
Andrea Asperti [Tue, 18 Dec 2012 11:33:44 +0000 (11:33 +0000)]
changes

11 years agochebyshev_teta
Andrea Asperti [Tue, 18 Dec 2012 11:33:24 +0000 (11:33 +0000)]
chebyshev_teta

11 years ago- lambda: some parts commented out, some refactoring
Ferruccio Guidi [Mon, 17 Dec 2012 22:24:07 +0000 (22:24 +0000)]
- lambda: some parts commented out, some refactoring
  and some notational changes
- lib: some additions from the preamble of "lambda"
- predefined_virtuals: some additions

11 years agoThis line, and those below, will be ignored--
Andrea Asperti [Mon, 17 Dec 2012 12:04:50 +0000 (12:04 +0000)]
This line, and those below, will be ignored--

D    arithmetics/big_pi.ma

11 years agosplitted chebyshev in two parts
Andrea Asperti [Mon, 17 Dec 2012 11:57:48 +0000 (11:57 +0000)]
splitted chebyshev in two parts

11 years agorestructuring
Andrea Asperti [Mon, 17 Dec 2012 11:08:59 +0000 (11:08 +0000)]
restructuring

11 years agobackup copy rm
Andrea Asperti [Mon, 17 Dec 2012 09:00:51 +0000 (09:00 +0000)]
backup copy rm

11 years agoStill porting chebyshev
Andrea Asperti [Mon, 17 Dec 2012 09:00:18 +0000 (09:00 +0000)]
Still porting chebyshev

11 years ago- we added delimiters to the URL in lambdadelta1
Ferruccio Guidi [Thu, 13 Dec 2012 16:00:39 +0000 (16:00 +0000)]
- we added delimiters to the URL in lambdadelta1

11 years ago- bib refactoring
Ferruccio Guidi [Wed, 12 Dec 2012 22:17:31 +0000 (22:17 +0000)]
- bib refactoring
- date correction for lambdadelta5

11 years agolambdadelta1 is now dated with release date of \lambda\delta version 1
Ferruccio Guidi [Wed, 12 Dec 2012 21:52:15 +0000 (21:52 +0000)]
lambdadelta1 is now dated with release date of \lambda\delta version 1

11 years ago- pointer structure simplified
Ferruccio Guidi [Tue, 11 Dec 2012 19:15:02 +0000 (19:15 +0000)]
- pointer structure simplified
- new properties on poiner orders
- last lemma in Kashima's article proved

11 years ago- lambda: - normalization theorem completed!
Ferruccio Guidi [Mon, 10 Dec 2012 20:54:24 +0000 (20:54 +0000)]
- lambda: - normalization theorem completed!
          - binary trees on pointer sequences set up to serve as labels for "st" computations
- lstar: right-oriened eliminator added

11 years agoPorting chebyshev
Andrea Asperti [Mon, 10 Dec 2012 08:56:30 +0000 (08:56 +0000)]
Porting chebyshev

11 years agoPorting chebyshev
Andrea Asperti [Mon, 10 Dec 2012 08:55:22 +0000 (08:55 +0000)]
Porting chebyshev

11 years ago- lambda: first half of the standardization theorem is proved!
Ferruccio Guidi [Sun, 9 Dec 2012 17:59:03 +0000 (17:59 +0000)]
- lambda: first half of the standardization theorem is proved!

11 years ago- list.ma: improved notation for constant lists (a "term 19" was missing)
Ferruccio Guidi [Sat, 8 Dec 2012 23:26:45 +0000 (23:26 +0000)]
- list.ma: improved notation for constant lists (a "term 19" was missing)
- lambda: more properties on pointers, extra xoa quantifier removed,
bugfix in notations and names

11 years ago- new pointes can point to any subterm
Ferruccio Guidi [Sat, 8 Dec 2012 14:54:25 +0000 (14:54 +0000)]
- new pointes can point to any subterm
- new star_ind_l-like eliminator for lstar now in use

11 years agolstar removed from list.ma and placed in its own file
Ferruccio Guidi [Fri, 7 Dec 2012 18:07:24 +0000 (18:07 +0000)]
lstar removed from list.ma and placed in its own file

11 years ago- "re": a part of reb.ma commented out since it cannot compile
Ferruccio Guidi [Fri, 7 Dec 2012 16:54:54 +0000 (16:54 +0000)]
- "re": a part of reb.ma commented out since it cannot compile

11 years ago- pts_dummy/pts_dummy_new: non compiling parts commented out
Ferruccio Guidi [Fri, 7 Dec 2012 16:36:51 +0000 (16:36 +0000)]
- pts_dummy/pts_dummy_new: non compiling parts commented out
- tutorial: some comments added

11 years ago- untranslated sections of "formal_topology" commented to make it compile
Ferruccio Guidi [Fri, 7 Dec 2012 14:30:36 +0000 (14:30 +0000)]
- untranslated sections of "formal_topology" commented to make it compile
- "tutorial" now compiles

11 years agomatch termination
Wilmer Ricciotti [Fri, 7 Dec 2012 13:09:32 +0000 (13:09 +0000)]
match termination

11 years ago- we enabled a notation for ex2
Ferruccio Guidi [Thu, 6 Dec 2012 16:10:57 +0000 (16:10 +0000)]
- we enabled a notation for ex2
- we improved star_ind_l that now behaves as if starl were defined
with a "left parameter" occurring on the right. this makes star_ind_l
symmetric with respect to star_ind
- we commented the non-more-compiling sections of "turing"
- some progress in "lambda"

11 years agoCleared unused variables in wsem_match (they were also sharing names with
Wilmer Ricciotti [Thu, 6 Dec 2012 15:40:58 +0000 (15:40 +0000)]
Cleared unused variables in wsem_match (they were also sharing names with
other variables).

11 years agoBug fixed: %n was badly failing (with Failure "nth") when n was
Claudio Sacerdoti Coen [Thu, 6 Dec 2012 13:03:09 +0000 (13:03 +0000)]
Bug fixed: %n was badly failing (with Failure "nth") when n was
not a valid constructor. Now fail is raised (to be captured by
try, etc.)

11 years agoFixes a bug in NCicElim.pp (term -> ast conversion used when building
Wilmer Ricciotti [Thu, 6 Dec 2012 09:48:53 +0000 (09:48 +0000)]
Fixes a bug in NCicElim.pp (term -> ast conversion used when building
projections) that was swapping arguments in a let-in, causing projection
generation to fail for any record field containing a let-in expression.

11 years agoConcludes match (weak) semantics. Yay!
Wilmer Ricciotti [Wed, 5 Dec 2012 11:07:28 +0000 (11:07 +0000)]
Concludes match (weak) semantics. Yay!

11 years agowe started Kashima's proof of standardization
Ferruccio Guidi [Tue, 4 Dec 2012 17:59:17 +0000 (17:59 +0000)]
we started Kashima's proof of standardization

11 years agomatch nearing completion
Wilmer Ricciotti [Tue, 4 Dec 2012 15:49:01 +0000 (15:49 +0000)]
match nearing completion

11 years agomatch wsem almost done
Wilmer Ricciotti [Tue, 4 Dec 2012 12:11:30 +0000 (12:11 +0000)]
match wsem almost done

11 years ago- nat.ma: we added a general induction principle
Ferruccio Guidi [Mon, 3 Dec 2012 19:41:24 +0000 (19:41 +0000)]
- nat.ma: we added a general induction principle
- lambda: we have the diamond property of parallel reduction
          notation bugfixes in term and muktiplicity

11 years ago- bugfix in stylesheets
Ferruccio Guidi [Sun, 2 Dec 2012 18:59:57 +0000 (18:59 +0000)]
- bugfix in stylesheets
- lddl data set released

11 years agobugfix in uri's: missing "/" added to baseuri's where necessary
Ferruccio Guidi [Sun, 2 Dec 2012 16:28:54 +0000 (16:28 +0000)]
bugfix in uri's: missing "/" added to baseuri's where necessary

11 years ago- dehypenation involves helena as well
Ferruccio Guidi [Sun, 2 Dec 2012 13:20:04 +0000 (13:20 +0000)]
- dehypenation involves helena as well
- now we compile helena against the latest version of matita components

11 years agothe dehyphenation update continues ...
Ferruccio Guidi [Sun, 2 Dec 2012 12:47:44 +0000 (12:47 +0000)]
the dehyphenation update continues ...

11 years agosome corrections to the prose of the web site
Ferruccio Guidi [Sun, 2 Dec 2012 12:28:43 +0000 (12:28 +0000)]
some corrections to the prose of the web site

11 years agoweb site update
Ferruccio Guidi [Sat, 1 Dec 2012 22:06:38 +0000 (22:06 +0000)]
web site update

11 years agoold lambdadelta home page is dismissed
Ferruccio Guidi [Sat, 1 Dec 2012 19:37:15 +0000 (19:37 +0000)]
old lambdadelta home page is dismissed

11 years agonug fix in the location of images
Ferruccio Guidi [Sat, 1 Dec 2012 18:51:12 +0000 (18:51 +0000)]
nug fix in the location of images

11 years ago- lambda: parallel reduction to obtain diamond property
Ferruccio Guidi [Sat, 1 Dec 2012 17:07:33 +0000 (17:07 +0000)]
- lambda: parallel reduction to obtain diamond property
- list:   local "norm" notation removed in favour of "card" core notation

11 years agoplanned dehyphenation of lambdadelta eventually took place!
Ferruccio Guidi [Sat, 1 Dec 2012 17:01:11 +0000 (17:01 +0000)]
planned dehyphenation of lambdadelta eventually took place!

11 years ago- bug fix in notation precedences
Ferruccio Guidi [Thu, 29 Nov 2012 16:53:26 +0000 (16:53 +0000)]
- bug fix in notation precedences
- bug fix in the Makefile