1 files changed, 12 insertions, 0 deletions

diff --git a/theories/util.v b/theories/util.v
new file mode 100644
index 0000000..c718622
--- /dev/null
+++ b/theories/util.v
@@ -0,0 +1,12 @@
+From iris.heap_lang Require Import notation.
+
+Definition loc_to_val (ℓ : loc) : val := #ℓ.
+Definition val_opt_hl (mv : option val) : val :=
+  match mv with
+  | None => NONEV
+  | Some v => SOMEV v
+  end.
+Definition loc_opt_hl : option loc → val :=
+  val_opt_hl ∘ fmap loc_to_val.
+Arguments loc_to_val _ / : assert.
+Arguments loc_opt_hl !_ / : assert.