Commit 2b7608f5 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Move an instance to its rightful place.

parent 63fa5416
Pipeline #42418 passed with stage
in 32 minutes and 26 seconds
......@@ -43,10 +43,6 @@ Hint Rewrite ly_size_PAGES_sub : refinedc_loc_eq_rewrite.
Hint Rewrite ly_size_PAGES : refinedc_loc_eq_rewrite.
Hint Rewrite ly_offset_PAGES : refinedc_loc_eq_rewrite.
Global Instance simpl_to_NULL_val_of_loc (l : loc):
SimplAndRel (=) NULL (l) (λ T, False).
Proof. split; naive_solver. Qed.
Section instances.
Context `{!typeG Σ}.
......
......@@ -30,3 +30,10 @@ Qed.
(** * location offset *)
Global Instance simpl_offset_inj l1 l2 sl n : SimplBothRel (=) (l1 at{sl} n) (l2 at{sl} n) (l1 = l2).
Proof. unfold GetMemberLoc. split; [apply shift_loc_inj1| naive_solver]. Qed.
(** * NULL *)
Global Instance simpl_to_NULL_val_of_loc (l : loc):
SimplAndRel (=) NULL (l) (λ T, False).
Proof. split; naive_solver. Qed.
Supports Markdown
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