val rw2rw : _: MiTLS.TLSConstants.rw -> MiTLS.Crypto.Indexing.rw
let rw2rw = function
  | TLSConstants.Reader -> Reader
  | TLSConstants.Writer -> Writer
module MiTLS.Crypto.Indexing
open MiTLS

open MiTLS.TLSInfo

type rw =
  | Reader
  | Writer
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked FStar.Pervasives.fsti.checked
MiTLS.Crypto.Indexing.fst
_: MiTLS.TLSConstants.rw -> MiTLS.Crypto.Indexing.rw
MiTLS.TLSConstants.rw MiTLS.Crypto.Indexing.Reader MiTLS.Crypto.Indexing.Writer MiTLS.Crypto.Indexing.rw
let rw2rw =
  
function
| TLSConstants.Reader -> Reader
| TLSConstants.Writer -> Writer