update in ground_2 and basic_2

frees_drops completed!

work in progress on frees_drops

MaTeX:
- notational macros for constants
- notational macro for quantification of propositions
matex.sty:
- support for math mode
- improved rendering of basic constructions
test style sheets
- some notational macros for legacy_1

- source web pages for lambdadelta_1
- minor bugs fixed in the web site

- update in ground_2 and basic_2
- updated documentation

frees_drops, initial versrion

some results on co-composition ...

more results on sor ...

initial support for lfpx_drops ...

more files missing :((

une file was missing :(

bug fixing ...

initial support for lfpx (replaces lpx and the parked llpx)

added config.ac to the tarball for debian packages

Was it really required? I don't know but it worked like that before.

initial support for LaTeX-defined notatopn

- support fof global alpha-conversion with hyperlinks
- Makefile: a bug fixed

update in basic_2

- notational change for cpg and cpx
- versions table updated on site

update in basic_2

- first results on cpx (dericed from those on cpg)
- minor bugs fixed

update in ground_2 and basic_2

bug fix in cpg allows to prove lsubr_cpg_trans

- ground_2: support for lifts_div4
- basic_2: cpg_drops competed

news for matita 0.99.3

the source code of matita 0.99.3 is online

bugfix ind docbook code for the relise of matita 0.99.3

some renaming and reordering of variables
the commit works up tp the "static" component + lpg.ma

pre commit for matita version 0.99.3

- matex: support for alpha-conversion completed
- matex.sty: hyperlinks without labels
- registry: support or triples

exportation of lambdadelta 1 with flavoured let recs

- partial commit of rt_transition  ...
- renaming in equivalence, dynamic, examples

milestone in basic_2 ...

ground_2: generic rt-transition counter

As required by M. Maietti,
cyclic sort hierarchies are now allowed through the "cyclic" keyword
so we can write:
universe cyclic constraint Type[U] < Type[U].
definition inconsistent: Type[U] ≝ Type[U].
matitaclean all is required after this commit

refactoring to park the notions:
lstas, unfold, crr, cir, cnr, crx, cix, cnx

universary milestone in basic_2

- former llpx_sn an lleq reactivated as lfxs and lfeq

- first working commit of the static component ..
- updates on some web pages

- advances on drops
- partial commit of the "static" component

renaming ...

minor additions :)

update in ground_2 and basic_2

- commit of the "s_computation" component ...
- additions in ground_2/relocation
- milestonee added in basic_2
- minor corrections

the newly generated web pages ...

- advances in the site generation architecture
- more on OSN and on the disclaimer

one file was missing

EBNF definition of OSN begins ...

- initial description of OSN
- ld_web: minor updates

images for Open Symbolic Notation (OSN)

update in ground_2 and basic_2 ...

- new component "s_transition" for the restored fqu and fquq
- minor additions
- notation update
- partial commit in the "static" component to park da and lsubd

- uniform relocations
- more results on at and after

minor correction on "source" production

minor additions ...

update in basic_2 and apps_2 ...

- minor corrections
- web pages for nasoc_2 and apps_2 are up again

another file was missing :(

- probe: now includes source character count (was: mac)
- lambdadelta: summaries are generated using the updated probe

support for printing the number of objects grouped by flavour

more files to commit .... :(

- ng_kernel: we print the offending term when guarded_by_constructors fails
- probe: we print the roots when more than one root is found
- lambdadelta: first working commit for the "relocation" component

update in ground_2

rtmaps with finite colength

advances in the theory of drops, lexs, and frees ...

- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
- source specifier on inductive/coinductive types (implies matitaclan all)
- minor additions

- ground_2: some additions
- basic_2/grammar: added missing files

partial commit in the relocation component to move some files ...

more results on after ...

small improvements and corrections ...

some corrections ...

mailstone in ground_2 ...

commitcompleted: some files were missing :(

rtmap (platform-indepent multple relocation): application and composition

- second precommit for rtmap
- we park relocation by streams of booleans

precommit for rtmap ...

MaTeX
- bug fixed in rendering of application: the head was not rendered sometimes
- we can generate the list of the produced TeX files
- TeX item for comments was missing
test
- bug fixed in matex.sty: pages were not ejected properly causig memory overflow
- now includes the whole \lambda\delta version 1 (737 pages for now)
- object numbering is now supported

now every object is output in a LaTeX environment, not just proofs

first commit for lreq ...

- ground_2: update ...
- basic_2: first commit for lexs ...

pre commit for lexs ...

general slicing reactivated ...

update in ground_2

- ground_2: support for relocation updated
- basic_2: theory of relocation updated
- MaTeX: (co)inductive types are now processed

- ground_2: relocation with nstream is now based on two basic functions (push and next)
- matex: scope management completed! stylesheet improved (also with colors)

- scope management completed
- improved style sheet and test document

- scope management begins...
- improved style sheet

improved style sheet

renaming ...

some renaming ...

lift functions and identity map

lexicon commands must tbe parsed before grafite commands rather than
after (why?)

documentation update

nstream: composition completed :)

ground_2: web page update

missing notation file

- ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i < 1)
- ground_1: relocation with streams of natural numbers begins

- plain anticipation for CIC proofs terms
- support for (co)fixpoint objects
- Makefile for testing
- minor updates

- Const is now processed properly

more minor bugs fixed in the web site