change operator

This commit is contained in:
Evgeny Poberezkin 2020-05-08 13:35:01 +01:00
parent b64a2e615d
commit 4a3e76cea1
2 changed files with 14 additions and 14 deletions

View file

@ -289,9 +289,9 @@ data Command : (ty : Type)
-> Command b from1 to2 state1 state3_fn
infix 5 &>
(&>) : (p : Participant)
infix 5 &:
(&:) : (p : Participant)
-> Command a from1 to1 state1 state2_fn
-> {auto prf : p = from1}
-> Command a from1 to1 state1 state2_fn
(&>) _ c = c
(&:) _ c = c

View file

@ -6,14 +6,14 @@ establishConnection : Command () Recipient Broker
(Null <==> (Null, 0) <==| Null)
(>>> Secured <==> (Secured, 0) <==| Secured)
establishConnection = do
Recipient &> CreateConn "recipient's public key for broker"
Recipient &> Subscribe
Recipient &> SendInvite newInvitation
Sender &> ConfirmConn "sender's public key for broker"
Broker &> PushConfirm
Recipient &> SecureConn "sender's public key for broker"
Sender &> SendWelcome
Broker &> PushWelcome
Sender &> SendMsg "Hello"
Broker &> PushMsg
Recipient &> DeleteMsg
Recipient &: CreateConn "recipient's public key for broker"
Recipient &: Subscribe
Recipient &: SendInvite newInvitation
Sender &: ConfirmConn "sender's public key for broker"
Broker &: PushConfirm
Recipient &: SecureConn "sender's public key for broker"
Sender &: SendWelcome
Broker &: PushWelcome
Sender &: SendMsg "Hello"
Broker &: PushMsg
Recipient &: DeleteMsg