Idris2Doc : Network.TLS.Parse.DER

Network.TLS.Parse.DER

(source)
Reexports
import public Utils.Time
Definitions
data TagType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Universal : TagType
  
Application : TagType
  
ContextSpecific : TagType
  
Private : TagType

  Hint: 
Show TagType
record Tag : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkTag : TagType -> Nat -> Tag

  Projections:
  
.tag_id : Tag -> Nat
  
.type : Tag -> TagType

  Hint: 
Show Tag
.type : Tag -> TagType
  Visibility: public export
type : Tag -> TagType
  Visibility: public export
.tag_id : Tag -> Nat
  Visibility: public export
tag_id : Tag -> Nat
  Visibility: public export
is_constructed : Bits8 -> Bool
  Visibility: export
record BitArray : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBitArray : Nat -> List Bits8 -> BitArray

  Projections:
  
.bytes : BitArray -> List Bits8
  
.padding : BitArray -> Nat

  Hint: 
Eq BitArray
.padding : BitArray -> Nat
  Visibility: public export
padding : BitArray -> Nat
  Visibility: public export
.bytes : BitArray -> List Bits8
  Visibility: public export
bytes : BitArray -> List Bits8
  Visibility: public export
data ASN1 : TagType -> Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Boolean : Bool -> ASN1 Universal 1
  
IntVal : Integer -> ASN1 Universal 2
  
Bitstring : BitArray -> ASN1 Universal 3
  
OctetString : List Bits8 -> ASN1 Universal 4
  
Null : ASN1 Universal 5
  
OID : List Nat -> ASN1 Universal 6
  
PrintableString : String -> ASN1 Universal 19
  
T61String : String -> ASN1 Universal 20
  
IA5String : String -> ASN1 Universal 22
  
UTF8String : String -> ASN1 Universal 12
  
Sequence : List (t : TagType ** (n : Nat ** ASN1 t n)) -> ASN1 Universal 16
  
Set : List (t : TagType ** (n : Nat ** ASN1 t n)) -> ASN1 Universal 17
  
UTCTime : DateTime -> ASN1 Universal 23
  
GeneralizedTime : DateTime -> ASN1 Universal 24
  
UnknownConstructed : (t : TagType) -> (n : Nat) -> List (t : TagType ** (n : Nat ** ASN1 t n)) -> ASN1 t n
  
UnknownPrimitive : (t : TagType) -> (n : Nat) -> List Bits8 -> ASN1 t n
constraint_parse : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) a -> Parser i (SimpleError String) (List a)
  Visibility: export
parse_length : (Monoid i, Cons (Posed Bits8) i) => Parser i (SimpleError String) Nat
  Visibility: export
parse_tag_id : (Monoid i, Cons (Posed Bits8) i) => Parser i (SimpleError String) (Bool, Tag)
  Visibility: export
signed_be_to_integer : List1 Bits8 -> Integer
  Visibility: export
decode_oid_nodes : Bits8 -> List Bits8 -> List Nat
  Visibility: export
parse_boolean : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) Bool
  Visibility: export
parse_integer : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) Integer
  Visibility: export
parse_bitarray : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) BitArray
  Visibility: export
parse_null : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) ()
  Visibility: export
parse_oid : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) (List Nat)
  Visibility: export
parse_time : (Cons (Posed Bits8) i, Monoid i) => Nat -> (String -> Either String DateTime) -> Parser i (SimpleError String) DateTime
  Visibility: export
parse_utf8 : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) String
  Visibility: export
ASN1Token : Type
  Visibility: public export
extract_string : ASN1Token -> Maybe String
  Visibility: export
extract_epoch : ASN1Token -> Maybe Integer
  Visibility: export
parse_asn1 : (Monoid i, Cons (Posed Bits8) i) => Parser i (SimpleError String) ASN1Token
  Visibility: export