val zip : (#a:Type) -> (#b:Type) -> l1:list a -> l2:list b ->
  Tot (l:list (a * b){L.length l == min (L.length l1) (L.length l2)})
let rec zip #a #b l1 l2 = match l1, l2 with
    | x::xs, y::ys -> (x,y) :: (zip xs ys)
    | _ -> []
val zip : (#a:Type) -> (#b:Type) -> l1:list a -> l2:list b ->
  Tot (l:list (a * b){L.length l == min (L.length l1) (L.length l2)})
let rec zip #a #b l1 l2 =
match l1, l2 with
| x :: xs, y :: ys -> (x, y) :: (zip xs ys)
| _ -> []
Pulse.Common.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Pulse.Common.fst
Prims.list FStar.Pervasives.Native.Mktuple2 Prims.Cons FStar.Pervasives.Native.tuple2 Pulse.Common.zip Prims.Nil Prims.eq2 Prims.int FStar.List.Tot.Base.length Prims.min
module Pulse.Common

module L = FStar.List.Tot
open FStar.Tactics

let (let?) (f:option 'a) (g:'a -> option 'b) : option 'b =
  match f with
  | None -> None
  | Some x -> g x

// let lem_bind_opt_some (x : option 'a) (f : 'a -> option 'b)
//   : Lemma (requires Some? ((let?) x f))
//           (ensures Some? x /\ Some? (f (Some?.v x)))
//           [SMTPat (Some? ((let?) x f))]
//   = ()

// let lem_bind_opt_none (x : option 'a) (f : 'a -> option 'b)
//   : Lemma (requires None? ((let?) x f))
//           (ensures None? x \/ None? (f (Some?.v x)))
//           [SMTPat (Some? ((let?) x f))]
//   = ()

let rec for_all_dec (top:'a) (l : list 'b{l << top}) (f : (x:'b{x << l} -> bool)) : bool =
  match l with
  | [] -> true
  | x::xs -> f x && for_all_dec top xs f

let rec map_dec (top:'a) (l : list 'b{l << top}) (f : (x:'b{x << l} -> 'c)) : list 'c =
  match l with
  | [] -> []
  | x::xs -> f x :: map_dec top xs f

let rec zipWith (f : 'a -> 'b -> Tac 'c) (l : list 'a) (m : list 'b)
  : Tac (l':(list 'c){L.length l' == min (L.length l) (L.length m)})
  =
  match l, m with
  | [], [] -> []
  | x::xs, y::ys -> f x y :: zipWith f xs ys
  | _ -> fail "zipWith: length mismatch"
  
val zip : (#a:Type) -> (#b:Type) -> l1:list a -> l2:list b ->
val zip : (#a:Type) -> (#b:Type) -> l1:list a -> l2:list b ->
  Tot (l:list (a * b){L.length l == min (L.length l1) (L.length l2)})
l1: Prims.list a -> l2: Prims.list b
  -> l:
    Prims.list (a * b)
      { FStar.List.Tot.Base.length l ==
        Prims.min (FStar.List.Tot.Base.length l1) (FStar.List.Tot.Base.length l2) }