diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-24 13:30:39 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-24 13:30:39 +0100 |
| commit | 2d7db0d8c48c41ecef78ef9f18253632a80f4710 (patch) | |
| tree | 39252b0237db5e1891da79b3203232abd27d2d14 /FinMap.agda | |
| parent | 88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907 (diff) | |
| download | bidiragda-2d7db0d8c48c41ecef78ef9f18253632a80f4710.tar.gz | |
prove theorem-2 in the presence of delete
The biggest piece of this puzzle was establishing
get <$> mapMV f v == mapMV f (get v)
provided that the result of mapMV is just something.
lemma-union-not-used lost a "map just", but could be retained in
structure.
Diffstat (limited to 'FinMap.agda')
0 files changed, 0 insertions, 0 deletions