let string_of_alert (a:alert) = 
  "level="^string_of_alertLevel a.level^
  "description="^string_of_alertDescription a.description
let string_of_alert (a: alert) =
"level=" ^ string_of_alertLevel a.level ^ "description=" ^ string_of_alertDescription a.description
TLSError.fst.checked
prims.fst.checked Parsers.AlertLevel.fsti.checked Parsers.AlertDescription.fsti.checked Parsers.Alert.fsti.checked FStar.String.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked
TLSError.fst
Parsers.Alert.alert Prims.op_Hat TLSError.string_of_alertLevel Parsers.Alert.__proj__Mkalert__item__level TLSError.string_of_alertDescription Parsers.Alert.__proj__Mkalert__item__description Prims.string
﻿module TLSError
open FStar.String
(* TLS explicitly returns run-time errors:
   results carry either values or error descriptions *)

include Parsers.AlertDescription
include Parsers.AlertLevel
include Parsers.Alert

let string_of_alertDescription (a:alertDescription) = "alertDescription"
let string_of_alertLevel (a:alertLevel) = "alertLevel"
val string_of_alert : a: Parsers.Alert.alert -> Prims.string
a: Parsers.Alert.alert -> Prims.string