val parse_algorithmIdentifier_payload
: parser (parse_algorithmIdentifier_payload_kind) (algorithmIdentifier_payload_t)
val parse_algorithmIdentifier_payload
: parser (parse_algorithmIdentifier_payload_kind) (algorithmIdentifier_payload_t)
let parse_algorithmIdentifier_payload
= parse_asn1_oid_TLV_of OID_ED25519
  `parse_synth`
  synth_algorithmIdentifier_payload_t
module X509.Crypto.AlgorithmIdentifier
open ASN1.Spec
open ASN1.Low

open X509.Base

open FStar.Integers

#set-options "--z3rlimit 32"
(* AlgorithmIdentifiers
  ======================
  NOTE: Different algorithms have identifiers in different structure.
*)
/
X509.Base.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.Crypto.AlgorithmIdentifier.fst
LowParse.Spec.Base.parser X509.Crypto.AlgorithmIdentifier.parse_algorithmIdentifier_payload_kind
  X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_payload_t
LowParse.Spec.Combinators.parse_synth LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind ASN1.Spec.Value.OID.the_asn1_oid ASN1.Base.OID_ED25519 X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_payload_t ASN1.Spec.Value.OID.parse_asn1_oid_TLV_of X509.Crypto.AlgorithmIdentifier.synth_algorithmIdentifier_payload_t
let parse_algorithmIdentifier_payload =
  
(parse_asn1_oid_TLV_of OID_ED25519) `parse_synth` synth_algorithmIdentifier_payload_t