From 22e14c821c69d7f6882cc4294d72e98ee5d9b931 Mon Sep 17 00:00:00 2001 From: Evgeny Poberezkin <2769109+epoberezkin@users.noreply.github.com> Date: Thu, 7 May 2020 18:05:05 +0100 Subject: [PATCH] correction --- specification/Simplex/Messaging.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/Simplex/Messaging.idr b/specification/Simplex/Messaging.idr index b47b38f8ad..f100c827c8 100644 --- a/specification/Simplex/Messaging.idr +++ b/specification/Simplex/Messaging.idr @@ -89,7 +89,7 @@ data EstablishedCS : ConnectionState -> Type where EDrained : EstablishedCS Drained --- state-dependent types to represent connections for all participants +-- dependent types to represent connections for all participants data BrokerConn : (state : ConnectionState) -> {auto prf : BrokerCS state} -> Type where BCNew : (recipient : Conn) -> (senderId : String) -> BrokerConn New