val list_map (#a #b: Type) (f: (a -> Tot b)) (l: list a) : Tot (l': list b {l' == L.map f l})
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
val list_map (#a #b: Type) (f: (a -> Tot b)) (l: list a) : Tot (l': list b {l' == L.map f l})
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
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 Prims.Nil Prims.Cons LowParse.Spec.Enum.list_map Prims.eq2 FStar.List.Tot.Base.map
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)
val list_map (#a #b: Type) (f: (a -> Tot b)) (l: list a) : Tot (l': list b {l' == L.map f l})
f: (_: a -> b) -> l: Prims.list a -> l': Prims.list b {l' == FStar.List.Tot.Base.map f l}