File tree Expand file tree Collapse file tree 1 file changed +6
-0
lines changed
Expand file tree Collapse file tree 1 file changed +6
-0
lines changed Original file line number Diff line number Diff line change @@ -210,12 +210,16 @@ type MessagePacket (MessageType : Type) : Type := mkMessagePacket {
210210 message : MessageType;
211211};
212212
213+ open MessagePacket;
214+
213215type EnvelopedMessage (MessageType : Type) : Type :=
214216 mkEnvelopedMessage {
215217 sender : Maybe Nat;
216218 packet : MessagePacket MessageType;
217219 };
218220
221+ open EnvelopedMessage;
222+
219223type Timer (HandleType : Type): Type := mkTimer {
220224 time : Nat;
221225 handle : HandleType;
@@ -225,6 +229,8 @@ type Trigger (MessageType : Type) (HandleType : Type) :=
225229 | MessageArrived { envelope : EnvelopedMessage MessageType; }
226230 | Elapsed { timers : List (Timer HandleType) };
227231
232+ open Trigger;
233+
228234getMessageFromTrigger : {M H : Type} -> Trigger M H -> Maybe M
229235 | (MessageArrived@{
230236 envelope := (mkEnvelopedMessage@{
You can’t perform that action at this time.
0 commit comments