Idris2Doc : Network.TLS.Certificate

Network.TLS.Certificate

(source)
Definitions
data AttributeType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
CommonName : AttributeType
  
Organization : AttributeType
  
OrganizationUnit : AttributeType
  
Country : AttributeType
  
StateOrProvince : AttributeType
  
LocalityName : AttributeType
  
SerialNumber : AttributeType
  
UnknownAttr : List Nat -> AttributeType

  Hints:
  
Eq AttributeType
  
Generic AttributeType [[], [], [], [], [], [], [], [List Nat]]
  
Meta AttributeType [[], [], [], [], [], [], [], [List Nat]]
  
Show AttributeType
from_oid_attr : List Nat -> AttributeType
  Visibility: export
record RelativeDistinguishedName : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkRDN : List (AttributeType, String) -> RelativeDistinguishedName

  Projection: 
.attributes : RelativeDistinguishedName -> List (AttributeType, String)

  Hint: 
Eq RelativeDistinguishedName
.attributes : RelativeDistinguishedName -> List (AttributeType, String)
  Visibility: public export
attributes : RelativeDistinguishedName -> List (AttributeType, String)
  Visibility: public export
record DistinguishedName : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDN : List RelativeDistinguishedName -> DistinguishedName

  Projection: 
.rdns : DistinguishedName -> List RelativeDistinguishedName

  Hints:
  
Eq DistinguishedName
  
Show DistinguishedName
.rdns : DistinguishedName -> List RelativeDistinguishedName
  Visibility: public export
rdns : DistinguishedName -> List RelativeDistinguishedName
  Visibility: public export
dn_attributes : DistinguishedName -> List (AttributeType, String)
  Visibility: export
data ExtensionType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
BasicConstraint : ExtensionType
  
KeyUsage : ExtensionType
  
SubjectAltName : ExtensionType
  
AuthorityKeyIdentifier : ExtensionType
  
UnknownExt : List Nat -> ExtensionType

  Hints:
  
DecEq ExtensionType
  
Eq ExtensionType
  
Generic ExtensionType [[], [], [], [], [List Nat]]
  
Meta ExtensionType [[], [], [], [], [List Nat]]
  
Show ExtensionType
record ExtBasicConstraint : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkExtBasicConstraint : Bool -> Maybe Nat -> ExtBasicConstraint

  Projections:
  
.ca : ExtBasicConstraint -> Bool
  
.path_len : ExtBasicConstraint -> Maybe Nat
.ca : ExtBasicConstraint -> Bool
  Visibility: public export
ca : ExtBasicConstraint -> Bool
  Visibility: public export
.path_len : ExtBasicConstraint -> Maybe Nat
  Visibility: public export
path_len : ExtBasicConstraint -> Maybe Nat
  Visibility: public export
record ExtKeyUsage : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkExtKeyUsage : Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> ExtKeyUsage

  Projections:
  
.crl_sign : ExtKeyUsage -> Bool
  
.data_encipherment : ExtKeyUsage -> Bool
  
.decipher_only : ExtKeyUsage -> Bool
  
.digital_signature : ExtKeyUsage -> Bool
  
.encipher_only : ExtKeyUsage -> Bool
  
.key_agreement : ExtKeyUsage -> Bool
  
.key_cert_sign : ExtKeyUsage -> Bool
  
.key_encipherment : ExtKeyUsage -> Bool
  
.non_repudiation : ExtKeyUsage -> Bool
.digital_signature : ExtKeyUsage -> Bool
  Visibility: public export
digital_signature : ExtKeyUsage -> Bool
  Visibility: public export
.non_repudiation : ExtKeyUsage -> Bool
  Visibility: public export
non_repudiation : ExtKeyUsage -> Bool
  Visibility: public export
.key_encipherment : ExtKeyUsage -> Bool
  Visibility: public export
key_encipherment : ExtKeyUsage -> Bool
  Visibility: public export
.data_encipherment : ExtKeyUsage -> Bool
  Visibility: public export
data_encipherment : ExtKeyUsage -> Bool
  Visibility: public export
.key_agreement : ExtKeyUsage -> Bool
  Visibility: public export
key_agreement : ExtKeyUsage -> Bool
  Visibility: public export
.key_cert_sign : ExtKeyUsage -> Bool
  Visibility: public export
key_cert_sign : ExtKeyUsage -> Bool
  Visibility: public export
.crl_sign : ExtKeyUsage -> Bool
  Visibility: public export
crl_sign : ExtKeyUsage -> Bool
  Visibility: public export
.encipher_only : ExtKeyUsage -> Bool
  Visibility: public export
encipher_only : ExtKeyUsage -> Bool
  Visibility: public export
.decipher_only : ExtKeyUsage -> Bool
  Visibility: public export
decipher_only : ExtKeyUsage -> Bool
  Visibility: public export
data GeneralName : Type
  Totality: total
  Visibility: public export
  Constructors:
  
DNSName : String -> GeneralName
  
IPv4Addr : IPv4Addr -> GeneralName
  
IPv6Addr : IPv6Addr -> GeneralName
  
UnknownGN : ASN1Token -> GeneralName

  Hints:
  
Eq GeneralName
  
Show GeneralName
record ExtSubjectAltName : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkExtSubjectAltName : List GeneralName -> ExtSubjectAltName

  Projection: 
.general_names : ExtSubjectAltName -> List GeneralName
.general_names : ExtSubjectAltName -> List GeneralName
  Visibility: public export
general_names : ExtSubjectAltName -> List GeneralName
  Visibility: public export
record ExtAuthorityKeyIdentifier : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkExtAuthorityKeyIdentifier : Maybe (Vect 20 Bits8) -> List GeneralName -> Maybe Integer -> ExtAuthorityKeyIdentifier

  Projections:
  
.general_names : ExtAuthorityKeyIdentifier -> List GeneralName
  
.key_identifier : ExtAuthorityKeyIdentifier -> Maybe (Vect 20 Bits8)
  
.serial_number : ExtAuthorityKeyIdentifier -> Maybe Integer
.key_identifier : ExtAuthorityKeyIdentifier -> Maybe (Vect 20 Bits8)
  Visibility: public export
key_identifier : ExtAuthorityKeyIdentifier -> Maybe (Vect 20 Bits8)
  Visibility: public export
.general_names : ExtAuthorityKeyIdentifier -> List GeneralName
  Visibility: public export
general_names : ExtAuthorityKeyIdentifier -> List GeneralName
  Visibility: public export
.serial_number : ExtAuthorityKeyIdentifier -> Maybe Integer
  Visibility: public export
serial_number : ExtAuthorityKeyIdentifier -> Maybe Integer
  Visibility: public export
extension_type : ExtensionType -> Type
  Visibility: public export
record Extension : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkExt : (extension_id : ExtensionType) -> Bool -> extension_type extension_id -> Extension

  Projections:
  
.critical : Extension -> Bool
  
.extension_id : Extension -> ExtensionType
  
.value : ({rec:0} : Extension) -> extension_type (extension_id {rec:0})
.extension_id : Extension -> ExtensionType
  Visibility: public export
extension_id : Extension -> ExtensionType
  Visibility: public export
.critical : Extension -> Bool
  Visibility: public export
critical : Extension -> Bool
  Visibility: public export
.value : ({rec:0} : Extension) -> extension_type (extension_id {rec:0})
  Visibility: public export
value : ({rec:0} : Extension) -> extension_type (extension_id {rec:0})
  Visibility: public export
record Certificate : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCertificate : Integer -> DistinguishedName -> Integer -> Integer -> DistinguishedName -> PublicKey -> Vect 20 Bits8 -> SignatureParameter -> BitArray -> List Extension -> List Bits8 -> Certificate

  Projections:
  
.cert_public_key : Certificate -> PublicKey
  
.cert_public_key_id : Certificate -> Vect 20 Bits8
  
.extensions : Certificate -> List Extension
  
.issuer : Certificate -> DistinguishedName
  
.serial_number : Certificate -> Integer
  
.sig_parameter : Certificate -> SignatureParameter
  
.signature_value : Certificate -> BitArray
  
.subject : Certificate -> DistinguishedName
  
.tbs_raw_bytes : Certificate -> List Bits8
  
.valid_not_after : Certificate -> Integer
  
.valid_not_before : Certificate -> Integer

  Hint: 
Show Certificate
.serial_number : Certificate -> Integer
  Visibility: public export
serial_number : Certificate -> Integer
  Visibility: public export
.issuer : Certificate -> DistinguishedName
  Visibility: public export
issuer : Certificate -> DistinguishedName
  Visibility: public export
.valid_not_before : Certificate -> Integer
  Visibility: public export
valid_not_before : Certificate -> Integer
  Visibility: public export
.valid_not_after : Certificate -> Integer
  Visibility: public export
valid_not_after : Certificate -> Integer
  Visibility: public export
.subject : Certificate -> DistinguishedName
  Visibility: public export
subject : Certificate -> DistinguishedName
  Visibility: public export
.cert_public_key : Certificate -> PublicKey
  Visibility: public export
cert_public_key : Certificate -> PublicKey
  Visibility: public export
.cert_public_key_id : Certificate -> Vect 20 Bits8
  Visibility: public export
cert_public_key_id : Certificate -> Vect 20 Bits8
  Visibility: public export
.sig_parameter : Certificate -> SignatureParameter
  Visibility: public export
sig_parameter : Certificate -> SignatureParameter
  Visibility: public export
.signature_value : Certificate -> BitArray
  Visibility: public export
signature_value : Certificate -> BitArray
  Visibility: public export
.extensions : Certificate -> List Extension
  Visibility: public export
extensions : Certificate -> List Extension
  Visibility: public export
.tbs_raw_bytes : Certificate -> List Bits8
  Visibility: public export
tbs_raw_bytes : Certificate -> List Bits8
  Visibility: public export
certificate_subject_names : Certificate -> List GeneralName
  Visibility: export
is_self_signed : Certificate -> Bool
  Visibility: export
extract_extension : (type : ExtensionType) -> Certificate -> Maybe (extension_type type)
  Visibility: export
parse_certificate : List Bits8 -> Either String Certificate
  Visibility: export