matita.cs.unibo.it Git - helm.git/history - matita/matita/contribs/lambdadelta

]> matita.cs.unibo.it Git - helm.git/history - matita/matita/contribs/lambdadelta

[helm.git] / matita / matita / contribs / lambdadelta /

2014-04-20	Ferruccio Guidi	- name changes in the rediction rules	tree \| commitdiff
2014-04-18	Ferruccio Guidi	- the relation for pointwise extensions now takes a...	tree \| commitdiff
2014-04-16	Ferruccio Guidi	3rd anniversary milestone	tree \| commitdiff
2014-04-15	Ferruccio Guidi	- lazy extended reduction parked	tree \| commitdiff
2014-04-13	Ferruccio Guidi	we restored the strong normalization of extended comput...	tree \| commitdiff
2014-04-10	Ferruccio Guidi	commit completed: one file was missing :(	tree \| commitdiff
2014-04-10	Ferruccio Guidi	- some work on extensions:	tree \| commitdiff
2014-04-08	Ferruccio Guidi	some advances on pointwise union for local environments ...	tree \| commitdiff
2014-04-07	Ferruccio Guidi	some resuls on pointwise extensions (all of them are...	tree \| commitdiff
2014-04-05	Ferruccio Guidi	commit completed:	tree \| commitdiff
2014-04-02	Ferruccio Guidi	commit of the "computation" component with lazy pointwi...	tree \| commitdiff
2014-03-30	Ferruccio Guidi	update of the partial commit:	tree \| commitdiff
2014-03-25	Ferruccio Guidi	- partial commit: just the components below "computation"	tree \| commitdiff
2014-03-20	Ferruccio Guidi	continuing on lazy pointwise extensions ...	tree \| commitdiff
2014-03-19	Ferruccio Guidi	we begin to develop lazy pointwisee extensions ...	tree \| commitdiff
2014-03-11	Ferruccio Guidi	reaxiomatized lleq fixes a bug in it and allows to...	tree \| commitdiff
2014-03-10	Ferruccio Guidi	some additions ...	tree \| commitdiff
2014-03-08	Ferruccio Guidi	we define the lazy poinwise extension of a relation...	tree \| commitdiff
2014-03-08	Ferruccio Guidi	some corrections ...	tree \| commitdiff
2014-03-03	Ferruccio Guidi	some additions for the forthcoming presentation	tree \| commitdiff
2014-02-28	Ferruccio Guidi	- some corrections and additions	tree \| commitdiff
2014-02-24	Ferruccio Guidi	- we bypassed another false conjecture :) ...	tree \| commitdiff
2014-02-22	Ferruccio Guidi	addition of unused material :)	tree \| commitdiff
2014-02-22	Ferruccio Guidi	a wrong conjecture bypassed!	tree \| commitdiff
2014-02-21	Ferruccio Guidi	- main proposition on lsx finally proved!	tree \| commitdiff
2014-02-18	Ferruccio Guidi	- a reinforement in a lemma on ldrop allows to prove...	tree \| commitdiff
2014-02-16	Ferruccio Guidi	- improved definition of lsx allows more invariants	tree \| commitdiff
2014-02-11	Ferruccio Guidi	some advances on reduction	tree \| commitdiff
2014-02-04	Ferruccio Guidi	evaluation for context-sensitive extended substitution...	tree \| commitdiff
2014-02-03	Ferruccio Guidi	we start total substitution ...	tree \| commitdiff
2014-01-31	Ferruccio Guidi	some notation renamed and fixed	tree \| commitdiff
2014-01-30	Ferruccio Guidi	normal forms for extended substitution	tree \| commitdiff
2014-01-29	Ferruccio Guidi	bug fix in the notation of normal forms, now we specify...	tree \| commitdiff
2014-01-27	Ferruccio Guidi	some corrections ...	tree \| commitdiff
2014-01-20	Ferruccio Guidi	commit completed: now we support two versions of slicin...	tree \| commitdiff
2014-01-18	Ferruccio Guidi	- commit of the "reduction" component with two addition...	tree \| commitdiff
2014-01-17	Ferruccio Guidi	commit of the "unfold" component ...	tree \| commitdiff
2014-01-17	Ferruccio Guidi	commit of the "static" component	tree \| commitdiff
2014-01-17	Ferruccio Guidi	- commit of the "substitution" component	tree \| commitdiff
2014-01-16	Ferruccio Guidi	commit of the "relocation" component with the new defin...	tree \| commitdiff
2014-01-15	Ferruccio Guidi	we start a criterion on extended computation	tree \| commitdiff
2014-01-13	Ferruccio Guidi	some improvements on the relation lsx ...	tree \| commitdiff
2014-01-10	Ferruccio Guidi	new definition of lleq allows to complete the proof...	tree \| commitdiff
2014-01-09	Ferruccio Guidi	- ynat: some additions	tree \| commitdiff
2014-01-06	Ferruccio Guidi	one file was missing :)	tree \| commitdiff
2014-01-06	Ferruccio Guidi	- lleq now uses ynat	tree \| commitdiff
2014-01-05	Ferruccio Guidi	- new definition of lazy equivalence for local environm...	tree \| commitdiff
2014-01-03	Ferruccio Guidi	- extended multiple substitutions now uses bounds in...	tree \| commitdiff
2014-01-03	Ferruccio Guidi	more arithmetics for natural numbers with infinity ...	tree \| commitdiff
2013-12-28	Ferruccio Guidi	some improvements and new lemmas for	tree \| commitdiff
2013-12-26	Ferruccio Guidi	the theory of extended multiple substitution for therms...	tree \| commitdiff
2013-12-20	Ferruccio Guidi	theory of extended iterated substitution begins ...	tree \| commitdiff
2013-12-19	Ferruccio Guidi	theory of cpy is complete!	tree \| commitdiff
2013-12-19	Ferruccio Guidi	the theory of cpy continues ...	tree \| commitdiff
2013-12-17	Ferruccio Guidi	refinement for extended substitution completed	tree \| commitdiff
2013-12-16	Ferruccio Guidi	- lsubr moved down one component	tree \| commitdiff
2013-12-15	Ferruccio Guidi	eliminators of arited terms based on "big tree" proper...	tree \| commitdiff
2013-12-14	Ferruccio Guidi	one file was still missing	tree \| commitdiff
2013-12-14	Ferruccio Guidi	commit is now complete :)	tree \| commitdiff
2013-12-14	Ferruccio Guidi	- "big tree" theorem is now proved up to some conjectur...	tree \| commitdiff
2013-12-09	Ferruccio Guidi	- first results on strongly normalizing local environments	tree \| commitdiff
2013-12-06	Ferruccio Guidi	partial commit ...	tree \| commitdiff
2013-12-04	Ferruccio Guidi	third commutation property on lazy equivalence for	tree \| commitdiff
2013-12-04	Ferruccio Guidi	first and second commutation property on lazy equivalen...	tree \| commitdiff
2013-12-02	Ferruccio Guidi	- last patrtial commit of the "reduction" and "computat...	tree \| commitdiff
2013-12-02	Ferruccio Guidi	initial commit of the "rduction" component	tree \| commitdiff
2013-12-01	Ferruccio Guidi	commit of the "substitution" component and of some...	tree \| commitdiff
2013-12-01	Ferruccio Guidi	- improved arithmetics for natural numbers with infinity	tree \| commitdiff
2013-11-29	Ferruccio Guidi	addition for natural numbers with infinity	tree \| commitdiff
2013-11-28	Ferruccio Guidi	definition of equivalence for local environments,	tree \| commitdiff
2013-11-27	Ferruccio Guidi	web page for ground_2 and bugfixed statistics generatio...	tree \| commitdiff
2013-11-27	Ferruccio Guidi	strict order relation for natural numbers with inifinity	tree \| commitdiff
2013-11-26	Ferruccio Guidi	- natural numbers with infinity for lambdadelta	tree \| commitdiff
2013-11-25	Ferruccio Guidi	- xoa: the definitions file now includes the notations...	tree \| commitdiff
2013-11-03	Ferruccio Guidi	second and third commutation property on lazy equivalen...	tree \| commitdiff
2013-11-01	Ferruccio Guidi	- lambdadelta: first commutation property on lazy equiv...	tree \| commitdiff
2013-10-28	Ferruccio Guidi	lazy equivalence for local environments is now defined	tree \| commitdiff
2013-10-27	Ferruccio Guidi	- lambdadelta: tentative definition of lazy equivalence...	tree \| commitdiff
2013-10-26	Ferruccio Guidi	- bug fix in the connection between global and restrict...	tree \| commitdiff
2013-10-25	Ferruccio Guidi	- bug fix in the induction for the closure property	tree \| commitdiff
2013-10-24	Ferruccio Guidi	- "small step" version of "big tree" theorem proved	tree \| commitdiff
2013-10-19	Ferruccio Guidi	more results towards the "big-tree" theorem ...	tree \| commitdiff
2013-10-14	Ferruccio Guidi	strongly normalizing terms for big-tree reduction are...	tree \| commitdiff
2013-10-12	Ferruccio Guidi	some renaming ...	tree \| commitdiff
2013-10-11	Ferruccio Guidi	bug fix in supclosure allows alternative definition...	tree \| commitdiff
2013-10-08	Ferruccio Guidi	bugfix in possible alternative definition of fpbs	tree \| commitdiff
2013-10-07	Ferruccio Guidi	some improvements towards an alternative definition...	tree \| commitdiff
2013-10-06	Ferruccio Guidi	bug fix in big-tree reduction	tree \| commitdiff
2013-10-06	Ferruccio Guidi	- big-tree reduction is now based on extended reduction	tree \| commitdiff
2013-10-05	Ferruccio Guidi	final na,e for big-tree rediction and computation	tree \| commitdiff
2013-10-04	Ferruccio Guidi	lenv refinement for native validity removed from big...	tree \| commitdiff
2013-10-04	Ferruccio Guidi	- degree assignment, static type assignment, iterated...	tree \| commitdiff
2013-09-07	Ferruccio Guidi	previous commit continued :)	tree \| commitdiff
2013-09-07	Ferruccio Guidi	support for nat-labeled reflexive and transitive closur...	tree \| commitdiff
2013-08-09	Ferruccio Guidi	- test.ma on the disambiguation bug moved to ONAG ...	tree \| commitdiff
2013-08-09	Ferruccio Guidi	- the example is now minimal so the bug is understood.	tree \| commitdiff
2013-08-09	Ferruccio Guidi	- the example is smaller and really self-contained ...	tree \| commitdiff
2013-08-09	Ferruccio Guidi	riduced example showing disambiguation bug ...	tree \| commitdiff
2013-08-09	Ferruccio Guidi	- matitadep: new option -t to list the unreferenced...	tree \| commitdiff
2013-08-07	Ferruccio Guidi	passive support for global environments completed!	tree \| commitdiff
next

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom