val prot:Type u#1
let prot : Type u#1 = protocol unit
val prot:Type u#1
let prot:Type u#1 =
protocol unit
Steel.Channel.Simplex.fsti.checked
Steel.Memory.fsti.checked Steel.Effect.fsti.checked Steel.Channel.Protocol.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Steel.Channel.Simplex.fsti
Steel.Channel.Protocol.protocol Prims.unit
(*
   Copyright 2020 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module Steel.Channel.Simplex
open Steel.Channel.Protocol
open Steel.Memory
open Steel.Effect

/// This library provides a model of unidirectional, protocol-indexed channels.
/// One party is allowed to send messages on the channel, while the other is allowed
/// to receive messages on the same channel.
/// Protocols are specified using the structure in Steel.Channel.Protocol


/// Msg int (fun x -> Msg (y:int { y > x }) (fun _ -> Ret unit))
///
val prot:Type u#1
Type