| 2008-09-12 |
Claudio Sacerdoti... | 1) as usual, I took the reverse notation for composition. |
tree | commitdiff |
| 2008-09-09 |
Claudio Sacerdoti... | Reordering of lemmas in proper places. |
tree | commitdiff |
| 2008-09-09 |
Claudio Sacerdoti... | Concrete spaces do form a category, after all :-) |
tree | commitdiff |
| 2008-09-09 |
Claudio Sacerdoti... | Getting closer thanks to more technical arrangements. |
tree | commitdiff |
| 2008-09-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-08 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-08 |
Claudio Sacerdoti... | Concrete spaces now defined. |
tree | commitdiff |
| 2008-09-05 |
Enrico Tassi | unification+pullback fix. It used to saturate a coercio... |
tree | commitdiff |
| 2008-09-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | fixed notation |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | restored |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | .... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | removed old non-working file |
tree | commitdiff |
| 2008-09-03 |
Claudio Sacerdoti... | Setoids are now more pervasive. |
tree | commitdiff |
| 2008-08-31 |
Claudio Sacerdoti... | Relations are now closer to Sambin's ones. I.e. they... |
tree | commitdiff |
| 2008-08-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-08-27 |
Claudio Sacerdoti... | Convergence is now defined. |
tree | commitdiff |
| 2008-08-27 |
Claudio Sacerdoti... | Better notation, in particular for subset comprehension. |
tree | commitdiff |
| 2008-08-26 |
Claudio Sacerdoti... | Notation |.| moved to core_notation. |
tree | commitdiff |
| 2008-08-25 |
Claudio Sacerdoti... | New categories REL and BP. |
tree | commitdiff |
| 2008-08-25 |
Claudio Sacerdoti... | New cool "type-checking" notation using colors and... |
tree | commitdiff |
| 2008-08-23 |
Claudio Sacerdoti... | Definition of categories. |
tree | commitdiff |
| 2008-08-23 |
Claudio Sacerdoti... | Some notation moved to core_notation. |
tree | commitdiff |
| 2008-08-23 |
Claudio Sacerdoti... | Also create the graphviz graph. |
tree | commitdiff |
| 2008-08-16 |
Enrico Tassi | added interpretation for \naturals, \rationals, and... |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | remove bad aliases from toolbox |
tree | commitdiff |
| 2008-07-23 |
Claudio Sacerdoti... | Universe levels fixed. |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | In some universe, membership is a morphism. |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | Sambin's & Valentini's toolbox (???) |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | Dependencies removed. |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | New input notation for bottom-up tree construction... |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | Input notation. |
tree | commitdiff |
| 2008-07-17 |
Claudio Sacerdoti... | 1 => \\e |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | more notation moved to core notation, unification of... |
tree | commitdiff |
| 2008-07-11 |
Claudio Sacerdoti... | A very nice experiment using notation: we define the... |
tree | commitdiff |
| 2008-07-10 |
Enrico Tassi | more work on dama |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | better notation |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | minor fixes |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | More definitions, following Ciraulo's Phd Thesis "Const... |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | Compatibility finished. |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | Nice: cotransitivity proved. |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | More work. |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | First few lemmas. But I have some problems in making... |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | First experiment in Padua about formal topologies. |
tree | commitdiff |
| 2008-06-30 |
Enrico Tassi | some more work on q |
tree | commitdiff |
| 2008-06-26 |
Enrico Tassi | more work on q |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2008-06-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable... |
tree | commitdiff |
| 2008-06-13 |
Claudio Sacerdoti... | New lemma |
tree | commitdiff |
| 2008-06-13 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-06-12 |
Enrico Tassi | Testing some performance tricks by caching the list... |
tree | commitdiff |
| 2008-06-11 |
Claudio Sacerdoti... | New, much faster implementation of factorize. |
tree | commitdiff |
| 2008-06-09 |
Claudio Sacerdoti... | Most of the time, URIs can now be replaced with identif... |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required by elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | Generalize no more required for elim. |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | generalize no more useful for elim |
tree | commitdiff |
| 2008-06-06 |
Claudio Sacerdoti... | Even more Q stuff moved around. |
tree | commitdiff |
| 2008-06-06 |
Claudio Sacerdoti... | Even more Q stuff classified. |
tree | commitdiff |
| 2008-06-06 |
Claudio Sacerdoti... | more stuff moved around |
tree | commitdiff |
| 2008-06-06 |
Claudio Sacerdoti... | More Q stuff organized in a coherent way. |
tree | commitdiff |
| 2008-06-06 |
Claudio Sacerdoti... | First snapshot at trying to clean up the Q library. |
tree | commitdiff |
| 2008-06-06 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-06-06 |
Andrea Asperti | A new theorem |
tree | commitdiff |
| 2008-06-06 |
Andrea Asperti | cleanup |
tree | commitdiff |
| 2008-06-06 |
Andrea Asperti | Cleanup. |
tree | commitdiff |
| 2008-06-06 |
Claudio Sacerdoti... | sieve.ma now depends only on primes.ma |
tree | commitdiff |
| 2008-06-06 |
Andrea Asperti | Added frac.ma |
tree | commitdiff |
| 2008-06-06 |
Andrea Asperti | Added Qplus_andrea.ma |
tree | commitdiff |
| 2008-06-05 |
Claudio Sacerdoti... | Eratosthene's sieve factorized out of nat/bertrand... |
tree | commitdiff |
| 2008-06-03 |
Claudio Sacerdoti... | Some proofs on enumerator and denominator. |
tree | commitdiff |
| 2008-06-03 |
Claudio Sacerdoti... | More work on rational numbers with unique representations. |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | garbage removed |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | case not unfilding fixed |
tree | commitdiff |
| 2008-05-27 |
Enrico Tassi | CoRN moved in contribs |
tree | commitdiff |
| 2008-05-27 |
Enrico Tassi | auto calls cleanup\ |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent products in inductive types arities... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | more fix removed from types |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | more fix removed from types in proofs |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | added a simplify to prevent the generation of an ugly fix |
tree | commitdiff |
| next |
projects / helm.git / history