Commit e46a7529 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Introduce notation excl' (like Excl' and ExclNone').

parent b3891ed5
...@@ -3,7 +3,7 @@ From iris.algebra Require Import upred updates. ...@@ -3,7 +3,7 @@ From iris.algebra Require Import upred updates.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ !_ /.
Record auth (A : Type) := Auth { authoritative : option (excl A); auth_own : A }. Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
Add Printing Constructor auth. Add Printing Constructor auth.
Arguments Auth {_} _ _. Arguments Auth {_} _ _.
Arguments authoritative {_} _. Arguments authoritative {_} _.
...@@ -14,7 +14,7 @@ Notation "● a" := (Auth (Excl' a) ∅) (at level 20). ...@@ -14,7 +14,7 @@ Notation "● a" := (Auth (Excl' a) ∅) (at level 20).
(* COFE *) (* COFE *)
Section cofe. Section cofe.
Context {A : cofeT}. Context {A : cofeT}.
Implicit Types a : option (excl A). Implicit Types a : excl' A.
Implicit Types b : A. Implicit Types b : A.
Implicit Types x y : auth A. Implicit Types x y : auth A.
......
...@@ -9,6 +9,7 @@ Inductive excl (A : Type) := ...@@ -9,6 +9,7 @@ Inductive excl (A : Type) :=
Arguments Excl {_} _. Arguments Excl {_} _.
Arguments ExclBot {_}. Arguments ExclBot {_}.
Notation excl' A := (option (excl A)).
Notation Excl' x := (Some (Excl x)). Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot). Notation ExclBot' := (Some ExclBot).
......
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