*2014-03-07* |
Helmut Grohne | improve notation of theorem-1 using local bindings |
blob | commitdiff |

*2014-03-07* |
Helmut Grohne | use allFin rather than tabulate id |
blob | commitdiff | diff to current |

*2014-03-05* |
Helmut Grohne | Merge branch feature-omit-sequence into master |
blob | commitdiff | diff to current |

*2014-03-04* |
Helmut Grohne | make lemma-sequenceV-successful more precise |
blob | commitdiff | diff to current |

*2014-02-26* |
Helmut Grohne | weaken assumptions made by theorem-2 and asssoc-enough |
blob | commitdiff | diff to current |

*2014-02-26* |
Helmut Grohne | remove the sequenceV call from bff |
blob | commitdiff | diff to current |

*2014-02-24* |
Helmut Grohne | theorem-2 works with EqR rather than SetoidReasoning... |
blob | commitdiff | diff to current |

*2014-02-24* |
Helmut Grohne | generalize/weaken lemma-get-mapMV |
blob | commitdiff | diff to current |

*2014-02-24* |
Helmut Grohne | define mapMV via sequenceV |
blob | commitdiff | diff to current |

*2014-02-24* |
Helmut Grohne | generalize lemma-lookupM-assoc |
blob | commitdiff | diff to current |

*2014-02-21* |
Helmut Grohne | minor simplifications |
blob | commitdiff | diff to current |

*2014-02-21* |
Helmut Grohne | use map-Σ to simplify lemma-mapM-successful |
blob | commitdiff | diff to current |

*2014-02-17* |
Helmut Grohne | Merge branch feature-partial-getlen into master |
blob | commitdiff | diff to current |

*2014-02-17* |
Helmut Grohne | avoid useless repetition |
blob | commitdiff | diff to current |

*2014-02-14* |
Helmut Grohne | Merge branch feature-shape-update into master |
blob | commitdiff | diff to current |

*2014-02-10* |
Helmut Grohne | Merge branch master into feature-shape-update |
blob | commitdiff | diff to current |

*2014-02-07* |
Helmut Grohne | replace rewrite with cong where feasible |
blob | commitdiff | diff to current |

*2014-02-07* |
Helmut Grohne | allow shape shape updates in bff |
blob | commitdiff | diff to current |

*2014-02-05* |
Helmut Grohne | be more precise about which lookups we use |
blob | commitdiff | diff to current |

*2014-02-05* |
Helmut Grohne | add lemma-lookupM-fromFunc |
blob | commitdiff | diff to current |

*2014-02-04* |
Helmut Grohne | remove unused imports |
blob | commitdiff | diff to current |

*2014-02-04* |
Helmut Grohne | add convenience members to PartialVecVec.Get |
blob | commitdiff | diff to current |

*2014-02-04* |
Helmut Grohne | Merge branch feature-get-record into feature-partial... |
blob | commitdiff | diff to current |

*2014-02-03* |
Helmut Grohne | make things compile with 2.3.0.1 |
blob | commitdiff | diff to current |

*2014-02-03* |
Helmut Grohne | Merge branch feature-get-record into master |
blob | commitdiff | diff to current |

*2014-01-30* |
Helmut Grohne | fully allow partial get functions |
blob | commitdiff | diff to current |

*2014-01-30* |
Helmut Grohne | allow importing of Bidir without any postulates |
blob | commitdiff | diff to current |

*2014-01-30* |
Helmut Grohne | pass get functions as records |
blob | commitdiff | diff to current |

*2014-01-28* |
Helmut Grohne | improve readability using _∋_≈_ instead of Setoid._≈_ |
blob | commitdiff | diff to current |

*2014-01-28* |
Helmut Grohne | use the indexed version of the Vec Setoid |
blob | commitdiff | diff to current |

*2014-01-28* |
Helmut Grohne | cleanup unused function and import |
blob | commitdiff | diff to current |

*2014-01-27* |
Helmut Grohne | Merge branch feature-delete |
blob | commitdiff | diff to current |

*2014-01-27* |
Helmut Grohne | Merge branch feature-decsetoid |
blob | commitdiff | diff to current |

*2014-01-27* |
Helmut Grohne | cleanup unused functions and useless steps |
blob | commitdiff | diff to current |

*2014-01-24* |
Helmut Grohne | prove theorem-2 in the presence of delete |
blob | commitdiff | diff to current |

*2014-01-23* |
Helmut Grohne | generalize BFF and theorem-2 to arbitrary Setoids |
blob | commitdiff | diff to current |

*2014-01-23* |
Helmut Grohne | show a stronger lemma-checkInsert-restrict |
blob | commitdiff | diff to current |

*2014-01-17* |
Helmut Grohne | generalize checkInsert to arbitrary Setoids |
blob | commitdiff | diff to current |

*2013-12-17* |
Helmut Grohne | refactor to get rid of FinMap without Maybe entirely |
blob | commitdiff | diff to current |

*2013-12-17* |
Helmut Grohne | update bff implementation to use delete |
blob | commitdiff | diff to current |

*2013-12-16* |
Helmut Grohne | move generic functions to a new Generic module |
blob | commitdiff | diff to current |

*2013-10-02* |
Helmut Grohne | need to fully qualify Data.List.All._::_ |
blob | commitdiff | diff to current |

*2013-07-21* |
Helmut Grohne | import _>>=_ and fmap from Data.Maybe |
blob | commitdiff | diff to current |

*2013-04-19* |
Helmut Grohne | move lemma-\notin-lookupM-assoc to Precond |
blob | commitdiff | diff to current |

*2013-04-10* |
Helmut Grohne | lemma-map-lookupM-assoc is even simpler |
blob | commitdiff | diff to current |

*2013-04-09* |
Helmut Grohne | rewrite lemma-map-lookupM-assoc |
blob | commitdiff | diff to current |

*2013-01-28* |
Helmut Grohne | drop the insert- prefix from the insertionresult ctors |
blob | commitdiff | diff to current |

*2013-01-17* |
Helmut Grohne | Merge branch view2 into master |
blob | commitdiff | diff to current |

*2013-01-14* |
Helmut Grohne | shrink lemma-union-not-used by matching on All's ctor |
blob | commitdiff | diff to current |

*2013-01-14* |
Helmut Grohne | define a more useful version of lemma-just\==nnothing |
blob | commitdiff | diff to current |

*2013-01-12* |
Helmut Grohne | introduce a proper view on checkInsert |
blob | commitdiff | diff to current |

*2013-01-10* |
Helmut Grohne | Merge branch 'newlemma' |
blob | commitdiff | diff to current |

*2013-01-10* |
Helmut Grohne | reduce a precondition of lemma-checkInsert-lookupM |
blob | commitdiff | diff to current |

*2013-01-09* |
Helmut Grohne | rewrite lemma-\notin-lookupM-assoc |
blob | commitdiff | diff to current |

*2013-01-05* |
Helmut Grohne | shrink lemma-union-not-used using cong\_2 |
blob | commitdiff | diff to current |

*2013-01-05* |
Helmut Grohne | shrink lemma-map-lookupM-insert using cong\_2 |
blob | commitdiff | diff to current |

*2013-01-05* |
Helmut Grohne | shrink base case of lemma-/notin-lookupM-assoc |
blob | commitdiff | diff to current |

*2012-12-10* |
Helmut Grohne | drop unused import |
blob | commitdiff | diff to current |

*2012-12-10* |
Helmut Grohne | drop unused param from lemma-map-lookupM-insert |
blob | commitdiff | diff to current |

*2012-12-06* |
Helmut Grohne | reduce useless case in lemma-map-lookupM-assoc |
blob | commitdiff | diff to current |

*2012-11-22* |
Helmut Grohne | shorten line lengths of theorem-2 |
blob | commitdiff | diff to current |

*2012-11-22* |
Helmut Grohne | shorten line length of theorem-1 |
blob | commitdiff | diff to current |

*2012-11-19* |
Helmut Grohne | turn lemma-fmap-just parameter into implicit |
blob | commitdiff | diff to current |

*2012-11-17* |
Helmut Grohne | strip prose from lemma-1 and lemma-2 |
blob | commitdiff | diff to current |

*2012-10-25* |
Helmut Grohne | similarly rename lemma-from-map-just to map-just-injective |
blob | commitdiff | diff to current |

*2012-10-25* |
Helmut Grohne | rename lemma-from-just to just-injective |
blob | commitdiff | diff to current |

*2012-10-22* |
Helmut Grohne | Merge branch 'modparam' |
blob | commitdiff | diff to current |

*2012-10-22* |
Helmut Grohne | finally parameterize CheckInsert |
blob | commitdiff | diff to current |

*2012-10-22* |
Helmut Grohne | now parameterize BFF |
blob | commitdiff | diff to current |

*2012-10-22* |
Helmut Grohne | parameterize Bidir via Carrier and deq |
blob | commitdiff | diff to current |

*2012-10-05* |
Helmut Grohne | move all postulates to one module |
blob | commitdiff | diff to current |

*2012-09-27* |
Helmut Grohne | move definition of get-type to BFF and use it everywhere |
blob | commitdiff | diff to current |

*2012-09-26* |
Helmut Grohne | use _\==n_ and _\notin_ instead of \neg |
blob | commitdiff | diff to current |

*2012-09-26* |
Helmut Grohne | import [_] instead of Reveal_is_ |
blob | commitdiff | diff to current |

*2012-09-18* |
Helmut Grohne | Merge branch 'using-vec' |
blob | commitdiff | diff to current |

*2012-09-17* |
Helmut Grohne | save a with in lemma-\inn-lookupM-assoc |
blob | commitdiff | diff to current |

*2012-09-14* |
Helmut Grohne | employ rewrite in lemma-map-lookupM-assoc |
blob | commitdiff | diff to current |

*2012-09-04* |
Helmut Grohne | rewrite main theorems to using Vec instead of List |
blob | commitdiff | diff to current |

*2012-06-05* |
Helmut Grohne | move bff and friends to submodule ListBFF |
blob | commitdiff | diff to current |

*2012-06-05* |
Helmut Grohne | move checkInsert and related properties to CheckInsert... |
blob | commitdiff | diff to current |

*2012-04-27* |
Helmut Grohne | lemma-2: do not confuse lookup with lookupM |
blob | commitdiff | diff to current |

*2012-04-27* |
Helmut Grohne | prove the theorem-2 |
blob | commitdiff | diff to current |

*2012-04-20* |
Helmut Grohne | remove lemma-\in-lookupM-assoc |
blob | commitdiff | diff to current |

*2012-04-20* |
Helmut Grohne | complete lemma-2 using new property _in-domain-of_ |
blob | commitdiff | diff to current |

*2012-04-19* |
Helmut Grohne | reduce hole in lemma-2 |
blob | commitdiff | diff to current |

*2012-04-19* |
Helmut Grohne | move lemma-just!=nothing to FinMap and use it there |
blob | commitdiff | diff to current |

*2012-04-17* |
Helmut Grohne | inline bot-elim into lemma-just-nothing |
blob | commitdiff | diff to current |

*2012-04-04* |
Helmut Grohne | abstract proofs over checkInsert |
blob | commitdiff | diff to current |

*2012-03-16* |
Helmut Grohne | fix wrong function name in lemma-2 |
blob | commitdiff | diff to current |

*2012-02-09* |
Helmut Grohne | remove useless braces |
blob | commitdiff | diff to current |

*2012-02-09* |
Helmut Grohne | s/generate/restrict/g |
blob | commitdiff | diff to current |

*2012-02-09* |
Helmut Grohne | rephrase free-theorem-list-list using pointwise equality |
blob | commitdiff | diff to current |

*2012-02-09* |
Helmut Grohne | formulate theorem-2 |
blob | commitdiff | diff to current |

*2012-02-09* |
Helmut Grohne | prove lemma-union-generate |
blob | commitdiff | diff to current |

*2012-02-09* |
Helmut Grohne | prove theorem-1 assuming a lemma-union-generate |
blob | commitdiff | diff to current |

*2012-02-09* |
Helmut Grohne | started proving theorem-1 |
blob | commitdiff | diff to current |

*2012-02-09* |
Helmut Grohne | introduce denumerate |
blob | commitdiff | diff to current |

*2012-01-31* |
Helmut Grohne | replace idrange with enumerate |
blob | commitdiff | diff to current |

*2012-01-31* |
Helmut Grohne | postulate free theorem for List a -> List a |
blob | commitdiff | diff to current |

*2012-01-26* |
Helmut Grohne | recursion of lemma-2 |
blob | commitdiff | diff to current |

next |