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.