add lemma-lookupM-fromFunc
[~helmut/bidiragda.git] / Precond.agda
2014-02-03 Helmut Grohnemake things compile with 2.3.0.1
2014-02-03 Helmut GrohneMerge branch feature-get-record into master
2014-01-30 Helmut Grohneallow importing of Bidir without any postulates
2014-01-30 Helmut Grohnepass get functions as records
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-23 Helmut Grohnegeneralize BFF and theorem-2 to arbitrary Setoids
2014-01-17 Helmut Grohnegeneralize checkInsert 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-07-21 Helmut Grohneimport _>>=_ and fmap from Data.Maybe
2013-04-19 Helmut Grohnemove lemma-\notin-lookupM-assoc to Precond
2013-04-14 Helmut Grohnesimpler formulation of All-different
2013-01-10 Helmut Grohneclean imports of Precond
2013-01-10 Helmut Grohneuse different formulation of all-different
2012-12-14 Helmut Grohneun-inline different-drop
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-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-09-27 Helmut Grohnemove definition of get-type to BFF and use it everywhere
2012-09-26 Helmut Grohnerename suc-\== to suc-injective
2012-09-18 Helmut GrohneMerge branch 'using-vec'
2012-09-08 Helmut Grohnegive a sufficient precondition for theorem-2