From 4a3e76cea1897a172c134fd4fd550065dd0f3c86 Mon Sep 17 00:00:00 2001 From: Evgeny Poberezkin <2769109+epoberezkin@users.noreply.github.com> Date: Fri, 8 May 2020 13:35:01 +0100 Subject: [PATCH] change operator --- specification/Simplex/Messaging/Protocol.idr | 6 ++--- specification/Simplex/Messaging/Scenarios.idr | 22 +++++++++---------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/specification/Simplex/Messaging/Protocol.idr b/specification/Simplex/Messaging/Protocol.idr index cdf82d11b8..4d07d32fd5 100644 --- a/specification/Simplex/Messaging/Protocol.idr +++ b/specification/Simplex/Messaging/Protocol.idr @@ -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 diff --git a/specification/Simplex/Messaging/Scenarios.idr b/specification/Simplex/Messaging/Scenarios.idr index 83e45482d9..92a07ac3d2 100644 --- a/specification/Simplex/Messaging/Scenarios.idr +++ b/specification/Simplex/Messaging/Scenarios.idr @@ -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