Network.TLS.Handle

Definitions

tls_version_to_state_type : TLSVersion -> Type

Visibility: public export

record TLSHandle : TLSVersion -> Type -> Type -> Type

Totality: total
Visibility: export
Constructor: 

MkTLSHandle : (1 _ : Handle t_ok t_closed (Res String (const t_closed)) (Res String (const t_closed))) -> tls_version_to_state_type version -> List Bits8 -> TLSHandle version t_ok t_closed

Projections:

.buffer : TLSHandle version t_ok t_closed -> List Bits8

.handle : TLSHandle version t_ok t_closed -> Handle t_ok t_closed (Res String (const t_closed)) (Res String (const t_closed))

.state : TLSHandle version t_ok t_closed -> tls_version_to_state_type version

Hints:

Uninhabited (TLSHandle TLS10 t_ok t_closed)

Uninhabited (TLSHandle TLS11 t_ok t_closed)

tls_handshake : {auto {conArg:6925} : (MonadRandom IO, LinearIO io)} -> ({arg:6929} : String) -> ({arg:6932} : List1 SupportedGroup) -> ({arg:6935} : List1 SignatureAlgorithm) -> ({arg:6938} : List1 CipherSuite) -> (1 {arg:6941} : Handle' t_ok t_closed) -> ({arg:6944} : CertificateCheck IO) -> L1 io (Res Bool (\ok => if ok then Handle' (TLSHandle' t_ok t_closed) t_closed else Res String (const t_closed)))

Visibility: export