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