diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-04-19 12:27:00 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-04-19 12:27:00 +0200 |
| commit | bf27d0ee5b48bfc843cdc9bd26b163e25a520df4 (patch) | |
| tree | 4f72d6783830c967a861f13d301975b0952af256 /CheckInsert.agda | |
| parent | fcf8bd5d0530dd6b05ba5c2931a66171b823e651 (diff) | |
| download | bidiragda-bf27d0ee5b48bfc843cdc9bd26b163e25a520df4.tar.gz | |
reduce hole in lemma-2
Introduce lemma-map-lookupM-assoc. It branches on whether the newly
inserted element is already present. To employ the results of this
branch two new lemmata lemma-\in-lookupM-assoc and
lemma-\notin-lookupM-assoc are used and they need
lemma-lookupM-checkInsert. The remaining hole in lemma-map-lookupM-assoc
targets the case where the checkInsert actually is an insert of a new
element. It probably needs more thinking to get this case right.
Diffstat (limited to 'CheckInsert.agda')
0 files changed, 0 insertions, 0 deletions