projects / ~helmut / bidiragda.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
make the Vec bff more similar to the List version
2012-06-05 Helmut Grohnemake the Vec bff more similar to the List version
 commit | commitdiff | tree
2012-06-05 Helmut Grohnedefine a bff over Vec
 commit | commitdiff | tree
2012-06-05 Helmut Grohnemove bff and friends to submodule ListBFF
 commit | commitdiff | tree
2012-06-05 Helmut Grohnemove checkInsert and related properties to CheckInsert...
commit | commitdiff | tree
2012-04-27 Helmut Grohnelemma-2: do not confuse lookup with lookupM
 commit | commitdiff | tree
2012-04-27 Helmut Grohneuse fromFunc to define union
 commit | commitdiff | tree
2012-04-27 Helmut Grohneprove the theorem-2
 commit | commitdiff | tree
2012-04-20 Helmut Grohneremove lemma-\in-lookupM-assoc
 commit | commitdiff | tree
2012-04-20 Helmut Grohnecomplete lemma-2 using new property _in-domain-of_
 commit | commitdiff | tree
2012-04-19 Helmut Grohnereduce hole in lemma-2
 commit | commitdiff | tree
2012-04-19 Helmut GrohneFinMap: lemma-lookupM-restrict drop useless implicit
 commit | commitdiff | tree
2012-04-19 Helmut Grohnemove lemma-just!=nothing to FinMap and use it there
 commit | commitdiff | tree
2012-04-17 Helmut Grohneinline bot-elim into lemma-just-nothing
 commit | commitdiff | tree
2012-04-04 Helmut Grohneabstract proofs over checkInsert
 commit | commitdiff | tree
2012-03-16 Helmut Grohnefix wrong function name in lemma-2
 commit | commitdiff | tree
2012-02-09 Helmut Grohneremove useless braces
 commit | commitdiff | tree
2012-02-09 Helmut Grohneavoid a sym in lemma-union-restrict
 commit | commitdiff | tree
2012-02-09 Helmut Grohnes/generate/restrict/g
 commit | commitdiff | tree
2012-02-09 Helmut Grohnerephrase free-theorem-list-list using pointwise equality
 commit | commitdiff | tree
2012-02-09 Helmut Grohneformulate theorem-2
 commit | commitdiff | tree
2012-02-09 Helmut Grohneprove lemma-union-generate
 commit | commitdiff | tree
2012-02-09 Helmut Grohneprove theorem-1 assuming a lemma-union-generate
 commit | commitdiff | tree
2012-02-09 Helmut Grohnestarted proving theorem-1
 commit | commitdiff | tree
2012-02-09 Helmut Grohneintroduce denumerate
 commit | commitdiff | tree
2012-01-31 Helmut Grohnereplace idrange with enumerate
 commit | commitdiff | tree
2012-01-31 Helmut Grohnepostulate free theorem for List a -> List a
 commit | commitdiff | tree
2012-01-26 Helmut Grohnerecursion of lemma-2
 commit | commitdiff | tree
2012-01-26 Helmut Grohnestarted proving lemma-2
 commit | commitdiff | tree
2012-01-26 Helmut Grohnereduce imports to speed up agda-mode
 commit | commitdiff | tree
2012-01-26 Helmut Grohnesplit Bidir.agda to FinMap.agda
 commit | commitdiff | tree
2012-01-26 Helmut Grohneimprove readability using spaces
 commit | commitdiff | tree
2012-01-26 Helmut Grohnereduce usage of sym
 commit | commitdiff | tree
2012-01-26 Helmut Grohneopen \==-Reasoning at top level
 commit | commitdiff | tree
2012-01-26 Helmut Grohneprove the remaining parts of lemma-checkInsert-generate
 commit | commitdiff | tree
2012-01-26 Helmut Grohnecomplete the yes part of lemma-checkInsert-generate...
commit | commitdiff | tree
2012-01-26 Helmut Grohnechange lemma-insert-same to work with \== proofs
 commit | commitdiff | tree
2012-01-23 Helmut Grohnebase case of lemma-2
 commit | commitdiff | tree
2012-01-23 Helmut Grohnerewrite lemma-1 using propositional equality
 commit | commitdiff | tree
2012-01-22 Helmut Grohneactually fmap is what I meant instead of >>=
 commit | commitdiff | tree
2012-01-22 Helmut Grohneintroduce >>= on Maybe to improve readability
 commit | commitdiff | tree
2012-01-22 Helmut Grohneimprove readability by introducing EqInst
 commit | commitdiff | tree
2012-01-22 Helmut Grohneformulate theorem-1
 commit | commitdiff | tree
2012-01-22 Helmut Grohneformulate lemma-2
 commit | commitdiff | tree
2012-01-22 Helmut Grohneattempt to prove lemma-1
 commit | commitdiff | tree
2012-01-21 Helmut Grohnerewrite generate using zip and fromAscList
 commit | commitdiff | tree
2012-01-21 Helmut Grohnesplit FinMap to FinMapMaybe
 commit | commitdiff | tree
2012-01-19 Helmut Grohnereplaced NatMap with FinMap
 commit | commitdiff | tree
2012-01-19 Helmut Grohnefirst attempt to define bff (with holes)
 commit | commitdiff | tree
2012-01-19 Helmut Grohneemploy standard library of agda where possible
 commit | commitdiff | tree
2012-01-19 Helmut Grohnefirst attempt to model lemma-1
 commit | commitdiff | tree
2012-01-19 Helmut Grohneadded .gitignore
 commit | commitdiff | tree
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)