2014-01-30 Helmut Grohnepass get functions as records
2014-01-30 Helmut Grohnesimplify compilation of the whole source
2014-01-28 Helmut Grohneimprove readability using _∋_≈_ instead of Setoid._≈_
2014-01-28 Helmut Grohnethere is no need to work with IsPreorder
2014-01-28 Helmut Grohneuse the indexed version of the Vec Setoid
2014-01-28 Helmut Grohnecleanup unused function and import
2014-01-27 Helmut GrohneMerge branch feature-delete
2014-01-27 Helmut GrohneMerge branch feature-decsetoid
2014-01-27 Helmut Grohnecleanup unused functions and useless steps
2014-01-27 Helmut Grohneprove assoc-enough in the presence of delete
2014-01-24 Helmut Grohneprove theorem-2 in the presence of delete
2014-01-23 Helmut Grohnegeneralize BFF and theorem-2 to arbitrary Setoids
2014-01-23 Helmut Grohneshow a stronger lemma-checkInsert-restrict
2014-01-17 Helmut Grohnegeneralize checkInsert to arbitrary Setoids
2014-01-17 Helmut Grohneshow that Vec is an indexed Setoid
2014-01-16 Helmut Grohnegeneralize lemma-insert-same to arbitrary Setoids
2013-12-17 Helmut Grohnerefactor to get rid of FinMap without Maybe entirely
2013-12-17 Helmut Grohneupdate bff implementation to use delete
2013-12-16 Helmut Grohneadd a mapM variant on the Maybe monad on Vecs
2013-12-16 Helmut Grohnemove generic functions to a new Generic module
2013-12-16 Helmut Grohneadd new functions delete, delete-many and partialize
2013-12-16 Helmut Grohneget rid of the ListBFF implementation
2013-10-02 Helmut Grohneneed to fully qualify Data.List.All._::_
2013-07-21 Helmut Grohneimport _>>=_ and fmap from Data.Maybe
2013-04-19 Helmut Grohnemove lemma-\notin-lookupM-assoc to Precond
2013-04-18 Helmut Grohnetrim lemma-union-restrict
2013-04-14 Helmut Grohnesimpler formulation of All-different
2013-04-10 Helmut Grohnelemma-map-lookupM-assoc is even simpler
2013-04-09 Helmut Grohnerewrite lemma-map-lookupM-assoc
2013-02-01 Helmut Grohneemploy insertionresult in lemma-lookupM-checkInsert
2013-01-28 Helmut Grohnedrop the insert- prefix from the insertionresult ctors
2013-01-28 Helmut Grohnepolish lemmata in FinMap
2013-01-17 Helmut GrohneMerge branch view2 into master
2013-01-14 Helmut Grohneshrink lemma-union-not-used by matching on All's ctor
2013-01-14 Helmut Grohnedefine a more useful version of lemma-just\==nnothing
2013-01-12 Helmut Grohneintroduce a proper view on checkInsert
2013-01-10 Helmut Grohneclean imports of Precond
2013-01-10 Helmut Grohneuse different formulation of all-different
2013-01-10 Helmut GrohneMerge branch 'newlemma'
2013-01-10 Helmut Grohnereduce a precondition of lemma-checkInsert-lookupM
2013-01-09 Helmut Grohnerewrite lemma-\notin-lookupM-assoc
2013-01-09 Helmut Grohneadd new lemma-checkInsert-lookupM
2013-01-09 Helmut Grohnesimplify lemma-lookupM-checkInsert using case-split
2013-01-05 Helmut Grohneshrink lemma-union-not-used using cong\_2
2013-01-05 Helmut Grohneshrink lemma-tabulate-\circ using cong\_2
2013-01-05 Helmut Grohneshrink lemma-map-lookupM-insert using cong\_2
2013-01-05 Helmut Grohneshrink base case of lemma-/notin-lookupM-assoc
2012-12-14 Helmut Grohneun-inline different-drop
2012-12-10 Helmut Grohnedrop unused import
2012-12-10 Helmut Grohneget rid of contraposition
2012-12-10 Helmut Grohnedrop unused param from lemma-map-lookupM-insert
2012-12-06 Helmut Grohnereduce useless case in lemma-map-lookupM-assoc
2012-11-22 Helmut Grohneshorten line length of lemma-lookupM-checkInsert
2012-11-22 Helmut Grohneshorten line lengths lemma-union-restrict
2012-11-22 Helmut Grohneshorten line lengths of theorem-2
2012-11-22 Helmut Grohneshorten line length of theorem-1
2012-11-19 Helmut Grohneturn lemma-fmap-just parameter into implicit
2012-11-19 Helmut Grohnewe can also drop an implicit parameter from assoc-enough
2012-11-19 Helmut Grohnewe can use one more \exists in assoc-enough
2012-11-19 Helmut Grohnestrip prose from assoc-enough
2012-11-17 Helmut Grohnestrip prose from lemma-1 and lemma-2
2012-11-02 Helmut Grohnerewrite checkInsert using "... |" notation
2012-10-25 Helmut Grohnesimilarly rename lemma-from-map-just to map-just-injective
2012-10-25 Helmut Grohnerename lemma-from-just to just-injective
2012-10-22 Helmut GrohneMerge branch 'modparam'
2012-10-22 Helmut Grohnefinally parameterize CheckInsert
2012-10-22 Helmut Grohnenow parameterize BFF
2012-10-22 Helmut Grohnealso parameterize Precond
2012-10-22 Helmut Grohneparameterize Bidir via Carrier and deq
2012-10-05 Helmut Grohnemove all postulates to one module
2012-10-05 Helmut Grohneremove VecRevBFF
2012-09-27 Helmut Grohneremove getVec-getlen in favour of plain subst
2012-09-27 Helmut Grohnemove definition of get-type to BFF and use it everywhere
2012-09-26 Helmut Grohneuse _\==n_ and _\notin_ instead of \neg
2012-09-26 Helmut Grohnerename suc-\== to suc-injective
2012-09-26 Helmut Grohneimport [_] instead of Reveal_is_
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-18 Helmut Grohneone more application of lemma-just\==nnothing
2012-09-17 Helmut Grohnesave a with in lemma-\inn-lookupM-assoc
2012-09-14 Helmut Grohneemploy rewrite in lemma-map-lookupM-assoc
2012-09-14 Helmut Grohne\::-subst is a special case of subst-cong
2012-09-14 Helmut Grohnevec-len-via-list and length-toList are the same
2012-09-14 Helmut Grohnecomplete missing parts of LiftGet
2012-09-11 Helmut Grohneshow fromList-toList in the subst form
2012-09-11 Helmut GrohneLiftGet: replace vec-length-same with toList-subst
2012-09-10 Helmut GrohneLiftGet: vec-length is also known as subst (Vec A)
2012-09-08 Helmut Grohnegive a sufficient precondition for theorem-2
2012-09-04 Helmut Grohnerewrite main theorems to using Vec instead of List
2012-09-04 Helmut Grohneformulate List <-> Vec isomorphism problems
2012-08-30 Helmut Grohneprove LiftGet.get-trafo-2-getlen
2012-08-30 Helmut Grohnephrase other half of bijection in LiftGet
2012-08-30 Helmut Grohneprove half of the bijection in LiftGet
2012-08-30 Helmut Grohnegive the type of different gets a name
2012-08-06 Helmut Grohneattempt isomorphism between get on List and on Vec
2012-06-19 Helmut Grohnethird definition of bff
2012-06-05 Helmut Grohnemake the Vec bff more similar to the List version
2012-06-05 Helmut Grohnedefine a bff over Vec
2012-06-05 Helmut Grohnemove bff and friends to submodule ListBFF
2012-06-05 Helmut Grohnemove checkInsert and related properties to CheckInsert...
2012-04-27 Helmut Grohnelemma-2: do not confuse lookup with lookupM