val map_flip_flip (#a #b: Type) (l: list (a * b)) : Lemma (list_map flip (list_map flip l) == l)
let rec map_flip_flip (#a #b: Type) (l: list (a * b)) : Lemma
  (list_map flip (list_map flip l) == l)
= match l with
  | [] -> ()
  | _ :: q -> map_flip_flip q
val map_flip_flip (#a #b: Type) (l: list (a * b)) : Lemma (list_map flip (list_map flip l) == l)
let rec map_flip_flip (#a #b: Type) (l: list (a * b)) : Lemma (list_map flip (list_map flip l) == l) =
match l with
| [] -> ()
| _ :: q -> map_flip_flip q
LowParse.Spec.Enum.fst.checked
prims.fst.checked LowParse.Spec.Combinators.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
LowParse.Spec.Enum.fst
Prims.list FStar.Pervasives.Native.tuple2 LowParse.Spec.Enum.map_flip_flip Prims.unit Prims.l_True Prims.squash Prims.eq2 LowParse.Spec.Enum.list_map LowParse.Spec.Enum.flip Prims.Nil FStar.Pervasives.pattern
module LowParse.Spec.Enum
include LowParse.Spec.Combinators

module L = FStar.List.Tot

[@Norm]
let rec list_map
  (#a #b: Type)
  (f: (a -> Tot b))
  (l: list a)
: Tot (l' : list b { l' == L.map f l } )
= match l with
  | [] -> []
  | a :: q -> f a :: list_map f q

type enum (key: eqtype) (repr: eqtype) = (l: list (key * repr) {
  L.noRepeats (list_map fst l) /\
  L.noRepeats (list_map snd l)
})

[@Norm]
let rec list_mem
  (#t: eqtype)
  (x: t)
  (l: list t)
: Tot (y: bool { y == true <==> L.mem x l == true } )
= match l with
  | [] -> false
  | a :: q -> (x = a || list_mem x q)

inline_for_extraction
let enum_key (#key #repr: eqtype) (e: enum key repr) : Tot eqtype = (s: key { list_mem s (list_map fst e) } )

inline_for_extraction
let make_enum_key (#key #repr: eqtype) (e: enum key repr) (k: key) : Pure (enum_key e)
  (requires (list_mem k (list_map fst e)))
  (ensures (fun k' -> k == (k' <: key)))
= k

inline_for_extraction
let enum_repr (#key #repr: eqtype) (e: enum key repr) : Tot eqtype = (r: repr { list_mem r (list_map snd e) } )

let flip (#a #b: Type) (c: (a * b)) : Tot (b * a) = let (ca, cb) = c in (cb, ca)

let rec map_flip_flip (#a #b: Type) (l: list (a * b)) : Lemma
val map_flip_flip (#a #b: Type) (l: list (a * b)) : Lemma (list_map flip (list_map flip l) == l)
l: Prims.list (a * b)
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Enum.list_map LowParse.Spec.Enum.flip
        (LowParse.Spec.Enum.list_map LowParse.Spec.Enum.flip l) ==
      l)