Commit 59444525 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename `fin_maps.singleton_proper` into `singletonM_proper`.

parent 5439c7d5
......@@ -57,6 +57,8 @@ Noteworthy additions and changes:
`seqZ_lookup_ge``lookup_seqZ_ge`, and `seqZ_lookup``lookup_seqZ`
+ Rename `lookup_seq_inv``lookup_seq` and generalize it to a bi-implication
+ Add `NoDup_seqZ` and `Forall_seqZ`
- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
`singletonM` and to avoid overlap with `sets.singleton_proper`.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
......
......@@ -184,7 +184,7 @@ Section setoid.
Global Instance insert_proper (i : K) :
Proper (() ==> () ==> (@{M A})) (insert i).
Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
Global Instance singleton_proper k : Proper (() ==> (@{M A})) (singletonM k).
Global Instance singletonM_proper k : Proper (() ==> (@{M A})) (singletonM k).
Proof.
intros ???; apply insert_proper; [done|].
intros ?. rewrite lookup_empty; constructor.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment