update in basic_2 ...

update in basic_2 and ground_2 ...

- improved fqu allows to prove fqu_cpx_trans and its derivatives
- parked frees_fqus_drops that does not hold anymore

update in basic_2 ...

- preservation of arity assignment
- hls orders files by extension and then by name

update in basic_2 ...

- improved lfpr_lfpr
- improved make stats (it was still invoking mac)
- hls.ml to list .ma files highligting the ones updated to basic_2A2

milestone in basic_2!

lfpx_frees and confluence of lfpr!

previous lemma proved ...

improved lsubf allowes to prove lsubf_frees_trans.

update in ground_2 and basic_2 ...

advances towards confluence of reduction in local environments ...

lexer updated with the new reference syntax +
linearized references updated in scripts

a linearized reference was still present ...

1) hard coded linearized references removed

2) new concrete syntax for linearized references
   more compliant with URI generic syntax and ELPI

   '#' not allowed in path and name

   Decl                   cic:/path/name#dec
   Def                    cic:/path/name#def:i
   Fix of int * int       cic:/path/name#fix:i:j:h
   CoFix of int           cic:/path/name#cfx:i
   Ind of int             cic:/path/name#ind:b:i:l
   Con of int * int       cic:/path/name#con:i:j:l

   run matitaclean all after this update,
   as stored aliases depend on linearized references

- basic_2 : restricted refinement for free variables (lsubf): first results
- ground_2: additions and corrections to sor

more on lfpx_frees.ma ...

- reconstruction of lfpx_frees.ma begins ...
- minor improvements

improved lexs_conf, now holds under weaker hypotheses ...

update in ground_2 and basic_2 ...

basic_2: stronger supclosure allows better inversion lemmas
ground_2: more results on sle and sor (rtmap)

some improvements towards the confluence of lfpr ...

milestone in basic_2!

one file was missing :(

diamond property of reduction!

first results on lfpr as a base for the diamond property ...

update in basic_2 ...

more results on cpm ...

one more paper citing \lambda\delta

update in ground_2 and basic_2

bug fix in the context reduction rule for cast (cpm)

we count rt parallel steps in a different way:
we use the maximum, that is idempotent, rather than the sum

xhtml simplified

more corrections to xhtml

corrected xhtml

site update

- initial page for osn ...
- some bug fixed

basic properties of cpr ...

- matex: notational macros for 0-ary constants
- stylesheets and Makefiles: minor improvements

- matex: we separate axioms (propositions) and assumptions (other)
- matex.sty: some improvements including
                  color for metalinguistic term constructions
- stylesheets: some improvements including more notation for basic_1

first definition of cpm:
the contextual rule for cast is incorrect :(

update in basic_2 ...

lfpx_drops completed!

totality of co-composition !

more notation for basic_1 ...

- matex: minor improvements
- latex stylesheets: more notation for basic_1
  now we use just the stix fonts

updating the dropable-related definitions with coafter ...

corrections to use less font packages (TeX was complaining)

- matex: minor corrections to handle applications with many arguments
- matex test stylesheets: some improvements, notation for ground_1 completed

does_not_occur documented

- improved support for case
- support for renaming constants

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 ...