add lemma-lookupM-fromFunc
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 5 Feb 2014 14:21:57 +0000 (15:21 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 5 Feb 2014 14:21:57 +0000 (15:21 +0100)
commitae6d9a356603e374c7d5b5693b318ecf0d2cc062
tree4efc111cad92b5be223a38e82563b9cc12de99df
parentaf563cc2bf8dfb20b88ad70a1e0fdd1dd3fa5ed1
add lemma-lookupM-fromFunc

The new lemma replaces two uses of lemma-fromFunc-tabulate, because the
latter exposes the implementation of FinMapMaybe, whereas the former
argues about the behaviour of FinMapMaybe. The aim of not exposing the
implementation (apart from brevity) is to enable refactoring.
Bidir.agda
FinMap.agda