Skip to content
Snippets Groups Projects
Commit e74d668a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix params & arguments of branch.

parent 4193e2e1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/channel/proto_channel.v
+ 2
− 1
View file @ e74d668a
...@@ -92,7 +92,8 @@ Definition iProto_branch {Σ} (a : action) (p1 p2 : iProto Σ) : iProto Σ := ...@@ -92,7 +92,8 @@ Definition iProto_branch {Σ} (a : action) (p1 p2 : iProto Σ) : iProto Σ :=
iProto_message a (tele_app (TT:=TeleS (λ _: bool, TeleO)) iProto_message a (tele_app (TT:=TeleS (λ _: bool, TeleO))
(λ b, (#b, True%I, if b then p1 else p2))). (λ b, (#b, True%I, if b then p1 else p2))).
Typeclasses Opaque iProto_branch. Typeclasses Opaque iProto_branch.
Instance: Params (@iProto_branch) 1. Arguments iProto_branch {_} _ _%proto _%proto.
Instance: Params (@iProto_branch) 2.
Infix "<+>" := (iProto_branch Send) (at level 85) : proto_scope. Infix "<+>" := (iProto_branch Send) (at level 85) : proto_scope.
Infix "<&>" := (iProto_branch Receive) (at level 85) : proto_scope. Infix "<&>" := (iProto_branch Receive) (at level 85) : proto_scope.
......
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