refactoring of \lambda\delta version 1 in matita

dependences update

dependences update

informational page on ground_1

basic_1: we separate theorems and lemmas as in basic_2
         the informational page is complete

update in web page for basic_1

- we add an informational page on \lambda\delta version 1 (core)
- web site update

lambdadelta_1: bugfix
Makefile: some improvements

infrastructure to browse lambdadelta_1 remotely

lambdadelta_1 updated with new part names

we restored the scripts of \lambda\delta version 1
(which are now available through \lambda\delta Web site)
by merging and updating all our (not broken) scripts

...

- xhtbl: minor improvement
- web site update
- static xhtml pages from lddl: updated trough ld_web infrastructure

last commit for helena 0.8.2
- a check was missing in the comparator
- new textual syntax for \lambda\delta "Version 4"
  (exp_math files updated accordingly)
- minor bug fixes (BrgOutput now uses the new alpha-conversion)

the corrected "Grundlagen" is online

lddl update with the disambiguated "grundlagen"

- bugfix is refreshed state of AutCrg: now we return a fresh state
- minor changes in the xml format
- some refactoring

removing some old files

finite lambda calculus

A compiling version

- bug fix in the RTM
- we can validate the Grundlagen in lambda-delta version 3

check removed

0.5.9 released

- we add the missing layer constraint on applicability condition
- trace levels refactoring

now type inclusion is correctly managed in the RTM

- we are moving from old (patched) management of sort inclusion
  to new (proper) one via \lambda\delta 3
- some refactoring
- omega.out: committed for reference
- Makefiles: some bugs fixed

- we removed a flag from the kernel status
- some renaming

- helena: the improved attribute system allows to export the sorts of Pi's
  Pi's of sort Prop are rendered as Forall's in the generated Matita script
- we updated the dtd accordingly

fixing

fixing

fixing

dependences update

level disambiguation cmpleted! the Grafite file is succesfully generated.
Matite cannot compiled it yet since it seems to freeze on notion 2760.
We divided the Grafite file in 7 parts for convenience.

- bug fix in the static disambiguation of unified binders
  allows to disambiguate the whole grundlagen
- 20 incompatibilities are detected (AutQE vs PTS)
- matita validates notion 115
- some refactoring

- the disambiguation of unified binders continues
- exportation to grafite is set up
- grundlagen_2: we disambiguate up to notion 6377, matita validates up
to notion 114

- ld.dtd updated
- basic2a.pdf updated
- documentation.html fixed

- static disambiguation of Automath unified binders
  by position heuristics + degree heuristics fixed
  [ grundlagen_2: now 1217 binders out of 47115 remain ambiguous ]
- brgReduction: we did not check the sort-inclusion flag
- new constraints system continues ...

- new attributes system
- new constraints system (starts)
- static disambiguation of Automath unified binders
  by degree heuristics (C.E. Brown)
  [ grundlagen_2: just 1960 binders out of 47115 remain ambiguous ]
- Makefile: XNLDIR is now relative

new intermediate language complete_rg,
more similar to what lambdadelta version 4 should be

new message reporting system improves performance significatively

- commit completed :)
typechecking is approx. fast as before,
validation is slightly faster than typechecking.
for now the new RTM is slightly slower than the old one
- we commit three versions of the grundlagen:
0 (original)
1 (no eta-conversion)
2 (no eta-conversion, no @-typing)

the commit contnues by updating the RTM and modifying the typechecker accordingly

the commit continues
computing the "ages" in the Automath component rather than in the brg kernel

the commit continues with some refactoring ...

the commit continues with the support for validation (inactive for now)

the partial commit continues
with the support for logging the e-reduction steps

we begin the commit of the validation procedure
(this includes some changes in the xml format of exported entities)
the procedure seems to introduce a delay, so this commit is partial ...

Web site update

web site updated with document J2

\lambda\delta version 2A released on Web site

- milestone update in basic_2 (basic_2a released)
- web site refactoring, update and bugfix

- the trace is explicit in all auto tactics with depth > 1
- one bug fixed
- the renaming continues ...

- some renaming according to the written version of basic_2
- more destructing lemmas invoked in place of buggy destructs

minor web site update

Typos.

- update in basic_2
- update of the web site: we added a "citations" section in the news

- grafiteParser: we added the comand "defined" as a presentational
alternative to "qed" for definitions.
- lambdadelta: we added an example about extended validity vs.
restricted validity + some minor corrections

more automation for cpcs ...

minor update in basic 2 and in the web site

update in basic_2 ...

- lambdadelta: minor corrections
- predefined_virtuals: some additions

we commit the web site again since last commit had some problems :(

old pabes removed

- update in basic_2
- web site major upddate

- some consequences of preservation added
- some renaming and some notation updated

catched typecheker failures in auto allow more applications of the tactic

contrib update ...

the commit was incomplete (as is often the case :( )

update in basic_2

- nnAuto: we catch TypeCheckerFailure generated at the end of
smart_apply (rel out of context) during equational reasoning,
and we treat it as an Error. TO BE UNDERSTTOD
(this TypeCheckerFailure dramatically interferes with automatic
proof search in \lambda\delta)
- lambdadelta: new definition of fpbg without fpbc + some refactoring

now the update is complete

previous commit was not complete :(

update in basic_2 ...

- fpbg can be reflexive (example given)
- so fpbu may use short steps rather than long steps
- some refactoring

minor update in basic_2 ...

notation update for pointwise union

big_O.ma

toolkit.ma

lablgtksourceview2 integrated into lablgtk2

minor update in basic_2 ...

notational change of lift, drop, and gget

update in basic_2 ...

slight refactoring in the proof of strong normalization

update in basic_2 ...

one more typo ...

bug fix in ththe notation for lists:
disambiguation of nil does not work very well in gcp_cr and gcp_aaa :(

...

...

added an example on lstas showing a difference with previous sta

- contrib update for version 2
- update in basic_2

New chapter on setoids.

chapter12 (coinductive) -> chapter13

milestone in basic_2 :)

commit completed! the new iterated static type assignment is up!

- the PARTIAL COMMIT continues, we issue the "reduction" component

- new stand-alone definition of lstas (sta and old lstas parked in etc)
- PARTIAL COMMIT: we issue just the components "static" and "unfold"

Notes.

A tentative chaptern on coinductive types.

Currently I hitted a major bug somewhere.

- update in basic_2
- minor update to the web site

some renaming and a minor addition