val sum_enum (t: sum) : Tot (enum (sum_key_type t) (sum_repr_type t))
let sum_enum (t: sum) : Tot (enum (sum_key_type t) (sum_repr_type t)) =
  match t with (Sum _ _ e _ _ _ _ _ _ _) -> e
val sum_enum (t: sum) : Tot (enum (sum_key_type t) (sum_repr_type t))
let sum_enum (t: sum) : Tot (enum (sum_key_type t) (sum_repr_type t)) =
match t with | Sum _ _ e _ _ _ _ _ _ _ -> e
LowParse.Spec.Sum.fst.checked
prims.fst.checked LowParse.Spec.Enum.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.Sum.fst
LowParse.Spec.Sum.sum Prims.eqtype LowParse.Spec.Enum.enum LowParse.Spec.Enum.enum_key LowParse.Spec.Base.refine_with_tag Prims.unit Prims.l_True Prims.squash Prims.eq2 LowParse.Spec.Sum.synth_case_recip' Prims.Nil FStar.Pervasives.pattern LowParse.Spec.Sum.sum_key_type LowParse.Spec.Sum.sum_repr_type
module LowParse.Spec.Sum
include LowParse.Spec.Enum

module Seq = FStar.Seq

let synth_case_recip'
    (#key: eqtype)
    (#repr: eqtype)
    (e: enum key repr)
    (#data: Type)
    (tag_of_data: (data -> Tot (enum_key e)))
    (type_of_tag: (enum_key e -> Tot Type))
    (synth_case_recip: ((k: enum_key e) -> (x: refine_with_tag tag_of_data k) -> Tot (type_of_tag k)))
    (x: data)
: GTot (type_of_tag (tag_of_data x))
= synth_case_recip (tag_of_data x) x

noeq
type sum =
| Sum:
    (key: eqtype) ->
    (repr: eqtype) ->
    (e: enum key repr) ->
    (data: Type) ->
    (tag_of_data: (data -> Tot (enum_key e))) ->
    (type_of_tag: (enum_key e -> Tot Type)) ->
    (synth_case: ((x: enum_key e) -> (y: type_of_tag x) -> Tot (refine_with_tag tag_of_data x))) ->
    (synth_case_recip: ((k: enum_key e) -> (x: refine_with_tag tag_of_data k) -> Tot (type_of_tag k))) ->
    (synth_case_recip_synth_case: (
      (x: enum_key e) ->
      (y: type_of_tag x) ->
      Lemma
      (synth_case_recip' e tag_of_data type_of_tag synth_case_recip (synth_case x y) == y)
    )) ->
    (synth_case_synth_case_recip: (
      (x: data) ->
      Lemma
      (synth_case (tag_of_data x) (synth_case_recip' e tag_of_data type_of_tag synth_case_recip x) == x)
    )) ->
    sum

inline_for_extraction
let sum_key_type (t: sum) : Tot eqtype =
  match t with (Sum key _ _ _ _ _ _ _ _ _) -> key

inline_for_extraction
let sum_repr_type (t: sum) : Tot eqtype =
  match t with (Sum _ repr _ _ _ _ _ _ _ _) -> repr

inline_for_extraction
val sum_enum (t: sum) : Tot (enum (sum_key_type t) (sum_repr_type t))
t: LowParse.Spec.Sum.sum
  -> LowParse.Spec.Enum.enum (LowParse.Spec.Sum.sum_key_type t) (LowParse.Spec.Sum.sum_repr_type t)