val list_mem (#t: eqtype) (x: t) (l: list t) : Tot (y: bool{y == true <==> L.mem x l == true})
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)
val list_mem (#t: eqtype) (x: t) (l: list t) : Tot (y: bool{y == true <==> L.mem x l == true})
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)
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.eqtype Prims.list Prims.op_BarBar Prims.op_Equality LowParse.Spec.Enum.list_mem Prims.bool Prims.l_iff Prims.eq2 FStar.List.Tot.Base.mem
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)
val list_mem (#t: eqtype) (x: t) (l: list t) : Tot (y: bool{y == true <==> L.mem x l == true})
x: t -> l: Prims.list t -> y: Prims.bool{y == true <==> FStar.List.Tot.Base.mem x l == true}