]> matita.cs.unibo.it Git - helm.git/history - matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
- advances on hereditarily free variables: now "frees" is primitive
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lleq.ma
2014-05-25 Ferruccio Guidi- theory of llor now includes (long awaited) non-recurs...
2014-04-25 Ferruccio Guidi- advances in the theory of cofrees
2014-04-18 Ferruccio Guidi- the relation for pointwise extensions now takes a...
2014-03-30 Ferruccio Guidiupdate of the partial commit:
2014-03-11 Ferruccio Guidireaxiomatized lleq fixes a bug in it and allows to...
2014-02-11 Ferruccio Guidisome advances on reduction
2014-01-31 Ferruccio Guidisome notation renamed and fixed
2014-01-18 Ferruccio Guidi- commit of the "reduction" component with two addition...
2014-01-17 Ferruccio Guidi- commit of the "substitution" component
2014-01-10 Ferruccio Guidinew definition of lleq allows to complete the proof...
2014-01-09 Ferruccio Guidi- ynat: some additions
2014-01-06 Ferruccio Guidi- lleq now uses ynat
2014-01-05 Ferruccio Guidi- new definition of lazy equivalence for local environm...