diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-04-20 11:55:52 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-04-20 11:55:52 +0200 |
| commit | b2eb5eef26787fcb9ff0778f82473b0fc2dc4caa (patch) | |
| tree | 23efdc8f8cd6028ec8e30b9b744a90b61a561497 /FinMap.agda | |
| parent | bf27d0ee5b48bfc843cdc9bd26b163e25a520df4 (diff) | |
| download | bidiragda-b2eb5eef26787fcb9ff0778f82473b0fc2dc4caa.tar.gz | |
complete lemma-2 using new property _in-domain-of_
Reasoning about assoc ... = just ... has turned out to be difficult for
inductive arguments. This is why I defined a new property between a List
(Fin n) and a FinMapMaybe n A. Thanks to Janis Voigtlaender for
suggesting this. lemma-assoc-domain transforms a property about assoc
into a domain property which can be used to complete the missing pieces
of lemma-2.
Diffstat (limited to 'FinMap.agda')
0 files changed, 0 insertions, 0 deletions