| 2008-07-15 |
Enrico Tassi | CProp_i <= Type_i , Type_i <= CProp_i
|
commit | commitdiff | tree |
| 2008-07-15 |
Enrico Tassi | models over N fixed
|
commit | commitdiff | tree |
| 2008-07-15 |
Enrico Tassi | new q_function representation
|
commit | commitdiff | tree |
| 2008-07-15 |
Enrico Tassi | removed dummy comment
|
commit | commitdiff | tree |
| 2008-07-15 |
Enrico Tassi | Using Prop conjuction on Props lowers the universes.
|
commit | commitdiff | tree |
| 2008-07-10 |
Enrico Tassi | value has a specification
|
commit | commitdiff | tree |
| 2008-07-10 |
Enrico Tassi | updated changelog
|
commit | commitdiff | tree |
| 2008-07-10 |
Enrico Tassi | more work on dama
|
commit | commitdiff | tree |
| 2008-07-10 |
Enrico Tassi | fixed regression in casting an argument to funclass...
|
commit | commitdiff | tree |
| 2008-07-09 |
Enrico Tassi | better notation
|
commit | commitdiff | tree |
| 2008-07-09 |
Enrico Tassi | minor fixes
|
commit | commitdiff | tree |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed:
|
commit | commitdiff | tree |
| 2008-07-09 |
Enrico Tassi | tab -> ' '
|
commit | commitdiff | tree |
| 2008-07-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-07-07 |
Enrico Tassi | simplified coercDb implementation with additional info...
|
commit | commitdiff | tree |
| 2008-07-03 |
Enrico Tassi | ...snapshot
|
commit | commitdiff | tree |
| 2008-07-03 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | some work
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | return 1 in case of failure
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | 0.5.2
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | 0.5.2
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-07-02 |
Enrico Tassi | calculation of the sort user to choose the rewriting...
|
commit | commitdiff | tree |
| 2008-07-01 |
Enrico Tassi | shifting done, merge attacked
|
commit | commitdiff | tree |
| 2008-07-01 |
Enrico Tassi | shift almost done
|
commit | commitdiff | tree |
| 2008-06-30 |
Enrico Tassi | new specification
|
commit | commitdiff | tree |
| 2008-06-30 |
Enrico Tassi | some more work on q
|
commit | commitdiff | tree |
| 2008-06-28 |
Enrico Tassi | some more work to factorize out uninteresting parts...
|
commit | commitdiff | tree |
| 2008-06-27 |
Enrico Tassi | more work to try to understand where the issue is
|
commit | commitdiff | tree |
| 2008-06-27 |
Enrico Tassi | lost in the wood
|
commit | commitdiff | tree |
| 2008-06-26 |
Enrico Tassi | more work
|
commit | commitdiff | tree |
| 2008-06-26 |
Enrico Tassi | few more steps
|
commit | commitdiff | tree |
| 2008-06-26 |
Enrico Tassi | more work
|
commit | commitdiff | tree |
| 2008-06-26 |
Enrico Tassi | some more work
|
commit | commitdiff | tree |
| 2008-06-26 |
Enrico Tassi | more work on q
|
commit | commitdiff | tree |
| 2008-06-25 |
Enrico Tassi | some more work
|
commit | commitdiff | tree |
| 2008-06-25 |
Enrico Tassi | better, reparsable, notation
|
commit | commitdiff | tree |
| 2008-06-24 |
Enrico Tassi | removed <_,_> notation second interpretation for dependent...
|
commit | commitdiff | tree |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and...
|
commit | commitdiff | tree |
| 2008-06-24 |
Enrico Tassi | missing file added
|
commit | commitdiff | tree |
| 2008-06-23 |
Enrico Tassi | more work, but russell too slow
|
commit | commitdiff | tree |
| 2008-06-23 |
Enrico Tassi | add \\ in front of tex macros
|
commit | commitdiff | tree |
| 2008-06-23 |
Enrico Tassi | notation support fixed to parentesize in a more sane...
|
commit | commitdiff | tree |
| 2008-06-23 |
Enrico Tassi | xxx
|
commit | commitdiff | tree |
| 2008-06-20 |
Enrico Tassi | left -> right
|
commit | commitdiff | tree |
| 2008-06-19 |
Enrico Tassi | fixed core notation
|
commit | commitdiff | tree |
| 2008-06-19 |
Enrico Tassi | notation fixed to be NON associative by default
|
commit | commitdiff | tree |
| 2008-06-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable...
|
commit | commitdiff | tree |
| 2008-06-18 |
Enrico Tassi | initial support for notation that specifies the precedence...
|
commit | commitdiff | tree |
| 2008-06-18 |
Enrico Tassi | removed unused variable
|
commit | commitdiff | tree |
| 2008-06-18 |
Enrico Tassi | some work on Q
|
commit | commitdiff | tree |
| 2008-06-17 |
Enrico Tassi | general reorganization and first (unconditional) proof...
|
commit | commitdiff | tree |
| 2008-06-17 |
Enrico Tassi | reordering of lexicon status partially avoided to make...
|
commit | commitdiff | tree |
| 2008-06-16 |
Enrico Tassi | Dedekind sigma completeness for the natural numbers.
|
commit | commitdiff | tree |
| 2008-06-16 |
Enrico Tassi | typo
|
commit | commitdiff | tree |
| 2008-06-13 |
Enrico Tassi | some notation added with a bit PITA
|
commit | commitdiff | tree |
| 2008-06-13 |
Enrico Tassi | when -debug do not catch
|
commit | commitdiff | tree |
| 2008-06-13 |
Enrico Tassi | when -debug do not catch
|
commit | commitdiff | tree |
| 2008-06-13 |
Enrico Tassi | replace assert false with AssertFailure
|
commit | commitdiff | tree |
| 2008-06-13 |
Enrico Tassi | more notation
|
commit | commitdiff | tree |
| 2008-06-13 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-06-13 |
Enrico Tassi | print the name not found in the env
|
commit | commitdiff | tree |
| 2008-06-12 |
Enrico Tassi | Testing some performance tricks by caching the list...
|
commit | commitdiff | tree |
| 2008-06-12 |
Enrico Tassi | better names in a lemma to increase readability
|
commit | commitdiff | tree |
| 2008-06-12 |
Enrico Tassi | fixed some regressions
|
commit | commitdiff | tree |
| 2008-06-11 |
Enrico Tassi | gran casino
|
commit | commitdiff | tree |
| 2008-06-11 |
Enrico Tassi | meta not considered before in outtype
|
commit | commitdiff | tree |
| 2008-06-10 |
Enrico Tassi | bla bla bla
|
commit | commitdiff | tree |
| 2008-06-10 |
Enrico Tassi | initial qork for models
|
commit | commitdiff | tree |
| 2008-06-10 |
Enrico Tassi | lebesgue proved
|
commit | commitdiff | tree |
| 2008-06-10 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2008-06-09 |
Enrico Tassi | initial work on lebesque
|
commit | commitdiff | tree |
| 2008-06-09 |
Enrico Tassi | exhaustivity completed
|
commit | commitdiff | tree |
| 2008-06-09 |
Enrico Tassi | exhaustivity, some work
|
commit | commitdiff | tree |
| 2008-06-07 |
Enrico Tassi | exhaustivity defined
|
commit | commitdiff | tree |
| 2008-06-07 |
Enrico Tassi | proof simplified
|
commit | commitdiff | tree |
| 2008-06-06 |
Enrico Tassi | lemma 3.6 subverted
|
commit | commitdiff | tree |
| 2008-06-05 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2008-06-05 |
Enrico Tassi | added order_continuity
|
commit | commitdiff | tree |
| 2008-06-05 |
Enrico Tassi | sandwich is back
|
commit | commitdiff | tree |
| 2008-06-03 |
Enrico Tassi | some work on uniformity
|
commit | commitdiff | tree |
| 2008-06-03 |
Enrico Tassi | end of section 2.2
|
commit | commitdiff | tree |
| 2008-06-03 |
Enrico Tassi | proof refactored
|
commit | commitdiff | tree |
| 2008-06-03 |
Enrico Tassi | xxx
|
commit | commitdiff | tree |
| 2008-06-01 |
Enrico Tassi | more work on supremum
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | CProp hierarchy is there!
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | irrelevance check half implemented but already impossible to
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | garbage removed
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | more work on dama
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | prod moved under lambda-prolog unification case
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | added CProp
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | thanks to the fact that we convert well typed term...
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | added a bit more reduction in case Prod v.s. term,...
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | relevance check partially implemented but bugged since...
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | case not unfilding fixed
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | CProp, since it was defined in CoRN as a Type, is predicative.
|
commit | commitdiff | tree |
| next |
projects / helm.git / search