Skip to content

GitLab

Commit a26a3367 authored by Ralf Jung's avatar Ralf Jung
Browse files

remark about one_shot

parent 245e0349
Hide whitespace changes
Inline Side-by-side
algebra/one_shot.v
View file @ a26a3367
...@@ -3,6 +3,7 @@ From iris.algebra Require Import upred. ...@@ -3,6 +3,7 @@ From iris.algebra Require Import upred.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
(* TODO: Really, we should have sums, and then this should be just "excl unit + A". *)
Inductive one_shot {A : Type} := Inductive one_shot {A : Type} :=
| OneShotPending : one_shot | OneShotPending : one_shot
| Shot : A → one_shot | Shot : A → one_shot
......
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