val fatalAlert : ad: MiTLS.Parsers.AlertDescription.alertDescription -> MiTLS.Parsers.Alert.alert
let fatalAlert ad = {level=Fatal; description=ad}
﻿module MiTLS.TLSError
open MiTLS
open FStar.String
(* TLS explicitly returns run-time errors:
   results carry either values or error descriptions *)

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

let string_of_alertDescription (a:alertDescription) = "alertDescription"
let string_of_alertLevel (a:alertLevel) = "alertLevel"
let string_of_alert (a:alert) = 
  "level="^string_of_alertLevel a.level^
  "description="^string_of_alertDescription a.description
/
prims.fst.checked MiTLS.Parsers.AlertLevel.fsti.checked MiTLS.Parsers.AlertDescription.fsti.checked MiTLS.Parsers.Alert.fsti.checked FStar.String.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked
MiTLS.TLSError.fst
ad: MiTLS.Parsers.AlertDescription.alertDescription -> MiTLS.Parsers.Alert.alert
MiTLS.Parsers.AlertDescription.alertDescription MiTLS.Parsers.Alert.Mkalert MiTLS.Parsers.AlertLevel.Fatal MiTLS.Parsers.Alert.alert
let fatalAlert ad =
  
{ level = Fatal; description = ad }