JoJoDeveloping

From iris.algebra Require Export ofe monoid cmra.
From iris.prelude Require Import options.
Locate pmap_omap.
Section restrict_validity.
  Definition restrictV (A : Type) (P : nat → A → Prop) := A.
  Local Instance restrictV_validN A P : ValidN (restrictV A P) := P.
  Local Instance restrictV_valid A P : Valid (restrictV A P) := λ a, ∀ n, P n a.

  Definition restrictV_cmra {A : cmra} PvalidN
  (* the new validity restricts the old one *)

JoJoDeveloping

From Coq Require Import Nat List Extraction. 
Import ListNotations.

Definition EqDec (A:Type) := forall (a b : A), {a = b} + {a <> b}.
Existing Class EqDec.
Definition eq_dec {A : Type} `{EqDec A} : EqDec A := _.

(* Defining these is somewhat annoying since you need to prove their correctness at the same time. *)
Program Instance eq_dec_option {A} {H : EqDec A} : EqDec (option A) := fun a b => match a, b with
  None, None => left _