search

kth-step / abs-metatheory

https://kth-step.github.io/abs-metatheory
MIT License
0 stars 0 forks source link

Extensional maps #14

Open Aqissiaq opened 6 months ago

Aqissiaq commented 6 months ago

Replace the non-extensional and semi-maintained FMaps with the extensional and recent Std++ finite maps described here:

palmskog commented 6 months ago

For the record, the general idiom for using finite maps via Std++ is the following:

From stdpp Require Import prelude fin_maps.

Section test.
Context `{FinMap K M}.

Definition test {A} (m : M A) (k : K) : option A := m !! k.
End test.