val zip (#a #b: _) (xs: list a) (ys: list b) : Tac (list (a & b))
let rec zip #a #b (xs: list a) (ys: list b): Tac (list (a & b)) =
  match xs, ys with
  | x :: xs, y :: ys -> (x, y) :: zip xs ys
  | [], [] -> []
  | _ -> fail "invalid argument: zip"
val zip (#a #b: _) (xs: list a) (ys: list b) : Tac (list (a & b))
let rec zip #a #b (xs: list a) (ys: list b) : Tac (list (a & b)) =
match xs, ys with
| x :: xs, y :: ys -> (x, y) :: zip xs ys
| [], [] -> []
| _ -> fail "invalid argument: zip"
Meta.Interface.fst.checked
prims.fst.checked Meta.Attribute.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.String.fsti.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.Pure.fst.checked FStar.List.fst.checked
Meta.Interface.fst
Prims.list FStar.Pervasives.Native.Mktuple2 Prims.Cons FStar.Pervasives.Native.tuple2 Meta.Interface.zip Prims.Nil FStar.Tactics.V1.Derived.fail
module Meta.Interface

open FStar.List.Tot
open FStar.Reflection
open FStar.Tactics

/// Local library
/// -------------

let assoc (#a: eqtype) #b (x: a) (l: list (a & b)): Tac b =
  match List.Tot.assoc x l with
  | Some x -> x
  | None -> fail "failure: assoc"
val zip (#a #b: _) (xs: list a) (ys: list b) : Tac (list (a & b))
xs: Prims.list a -> ys: Prims.list b -> FStar.Tactics.Effect.Tac (Prims.list (a * b))