diff --git a/algebra/one_shot.v b/algebra/one_shot.v index 65a96aa4dfb545ae030d80201e1af39b46ccaa00..14cb69b265f4f393cbef4f5078fbc71b8f35906a 100644 --- a/algebra/one_shot.v +++ b/algebra/one_shot.v @@ -3,6 +3,7 @@ From iris.algebra Require Import upred. Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. +(* TODO: Really, we should have sums, and then this should be just "excl unit + A". *) Inductive one_shot {A : Type} := | OneShotPending : one_shot | Shot : A → one_shot