Commit 8ada8daa authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'fix-for-stuck-classes' into 'master'

Fix two scripts due to bugfix in mode-checking

See merge request iris/iris!344
parents 335ff6d7 e9e6e220
Pipeline #22065 passed with stage
in 15 minutes and 50 seconds
......@@ -49,7 +49,7 @@ Global Instance lookup_ne k :
Proof. by intros m1 m2. Qed.
Global Instance lookup_proper k :
Proper (() ==> ()) (lookup k : gmap K A option A) := _.
Global Instance alter_ne f k n :
Global Instance alter_ne (f : A A) (k : K) n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (alter f k).
Proof.
intros ? m m' Hm k'.
......
......@@ -340,13 +340,13 @@ Section properties.
rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
Qed.
Lemma list_core_singletonM i (x : A) : core {[ i := x ]} {[ i := core x ]}.
Lemma list_core_singletonM i (x : A) : core {[ i := x ]} @{list A} {[ i := core x ]}.
Proof.
rewrite /singletonM /list_singletonM.
by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ).
Qed.
Lemma list_op_singletonM i (x y : A) :
{[ i := x ]} {[ i := y ]} {[ i := x y ]}.
{[ i := x ]} {[ i := y ]} @{list A} {[ i := x y ]}.
Proof.
rewrite /singletonM /list_singletonM /=.
induction i; constructor; rewrite ?left_id; auto.
......
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