diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-01-26 17:12:44 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-01-26 17:12:44 +0100 |
| commit | 5ece23e8705d2ea3128961a24baed6652383b1ad (patch) | |
| tree | 148625bc910dc5687e2da85e3fef493e91ec47be /FinMap.agda | |
| parent | 1e2ddab6a91377a939d47e30ed1575b03784a09f (diff) | |
| download | bidiragda-5ece23e8705d2ea3128961a24baed6652383b1ad.tar.gz | |
started proving lemma-2
The step case needs two lemmata. One for the head of the resulting map and one
for the tail. The head case is shown using a
lemma-lookupM-assoc : assoc eq (i :: _) (x :: _) == just h ->
lookupM i h == just x
Diffstat (limited to 'FinMap.agda')
0 files changed, 0 insertions, 0 deletions