Skip to content

Allow `map_imap` to be used in nested recursive fixpoints.

Robbert Krebbers requested to merge robbert/map_imap_nested_fixpoint into master

See the test file for an example.

I expect this change to be backwards compatible. Since the definition of map_imap is awful, I don't expect anyone to use it directly (i.e., perform unfold map_imap in proofs), but rather use map_lookup_imap or other lemmas.

Merge request reports