fact: Fixpoint ASN1_Structured_denote (desc : ASN1_Structured) : Set := match desc with | ASN_Sequence l => (fix ASN1_Sequence_denote (descs : list ASN1_Sequence_Element) {struct descs} : Set := match descs with | Normal_Sequence_Element desc :: descs' => (ASN1_Type_denote desc) * (ASN1_Sequence_denote descs') | Optional_Sequence_Element desc :: descs' => option (ASN1_Type_denote desc) * (ASN1_Sequence_denote descs') | Default_Sequence_Element desc _ _ :: descs' => (ASN1_Simple_denote desc) * (ASN1_Sequence_denote descs') | [ ] => unit end)%type l | ASN_Choice l => (fix ASN1_Choice_denote (descs : list ASN1_Type) {struct descs} : Set := match descs with | desc :: descs' => (ASN1_Type_denote desc) + (ASN1_Choice_denote descs') | [ ] => unit end)%type l | ASN_Sequence_Of desc' => list (ASN1_Type_denote desc') end with ASN1_Type_denote (desc : ASN1_Type) : Set := match desc with | ASN_Simple desc' mod => ASN1_Simple_denote desc' | ASN_Structured desc' => ASN1_Structured_denote desc' end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.Ascii Coq.Strings.String Coq.Numbers.BinNums Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts