From e2681e43cc7849d66425d5bc93565e9e177d229a Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Wed, 24 Jun 2026 19:29:28 +0200
Subject: Initial commit

---
 theories/util.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 theories/util.v

(limited to 'theories/util.v')

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.
-- 
cgit v1.3