Skip to content
Snippets Groups Projects
Commit 315ef81d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Simplify local update for excl

parent dbb8d7c9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
algebra/excl.v
+ 1
− 1
View file @ 315ef81d
...@@ -116,7 +116,7 @@ Proof. uPred.unseal. by destruct x. Qed. ...@@ -116,7 +116,7 @@ Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *) (** ** Local updates *)
Global Instance excl_local_update y : Global Instance excl_local_update y :
LocalUpdate (λ x, if x is Excl _ then ✓ y else False) (λ _, y). LocalUpdate (λ _, True) (λ _, y).
Proof. split. apply _. by destruct y; intros n [a|] [b'|]. Qed. Proof. split. apply _. by destruct y; intros n [a|] [b'|]. Qed.
(** Updates *) (** Updates *)
......
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