val synth_case_recip'
      (#key #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))
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
val synth_case_recip'
      (#key #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))
let synth_case_recip'
      (#key #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
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
Prims.eqtype LowParse.Spec.Enum.enum LowParse.Spec.Enum.enum_key LowParse.Spec.Base.refine_with_tag
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)
val synth_case_recip'
      (#key #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))

    e: LowParse.Spec.Enum.enum key repr ->
    tag_of_data: (_: data -> LowParse.Spec.Enum.enum_key e) ->
    type_of_tag: (_: LowParse.Spec.Enum.enum_key e -> Type) ->
    synth_case_recip:
      (k: LowParse.Spec.Enum.enum_key e -> x: LowParse.Spec.Base.refine_with_tag tag_of_data k
          -> type_of_tag k) ->
    x: data
  -> Prims.GTot (type_of_tag (tag_of_data x))