val mem (#a:eqtype) (#f:cmp a) (x:a) (s:mset a f) : nat
val mem (#a:eqtype) (#f:cmp a) (x:a) (s:mset a f) : nat
let rec mem #_ #_ x s =
  match s with
  | [] -> 0
  | (y, n)::_ -> if x = y then n else mem x (tl s)
module Zeta.MultiSet

open FStar.List.Tot


/// We represet a multiset with a sorted associative list
///   where the second component of each list element is the
///   cardinality of the first component in the set
///
/// The list is sorted on the first component of its elements


let rec sorted (#a:eqtype) (f:cmp a) (l:list (a & pos)) : Type0 =
  match l with
  | [] -> True
  | [_] -> True
  | (x, _)::(y, card_y)::tl ->
    f x y /\
    x =!= y /\
    sorted f ((y, card_y)::tl)

let mset a f = l:list (a & pos){sorted f l}


/// We will use this function, rather than pattern matching to get better implicit inference

let tl (#a:eqtype) (#f:cmp a) (s:mset a f{Cons? s}) : mset a f = tl s

let empty #_ #_ = []

let create #_ #_ x m = [x, m]
/
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Zeta.MultiSet.fst
x: a -> s: Zeta.MultiSet.mset a f -> Prims.nat
Prims.eqtype Zeta.MultiSet.cmp Zeta.MultiSet.mset Prims.pos Prims.list FStar.Pervasives.Native.tuple2 Prims.op_Equality Prims.bool Zeta.MultiSet.mem Zeta.MultiSet.tl Prims.nat
let rec mem #_ #_ x s =
  
match s with
| [] -> 0
| (y, n) :: _ -> if x = y then n else mem x (tl s)