val map2 (#a #b #c: _) (f: (a -> b -> Tac c)) (xs: list a) (ys: list b) : Tac (list c)
let rec map2 #a #b #c (f : a -> b -> Tac c) (xs : list a) (ys : list b) : Tac (list c) =
  match xs, ys with
  | [], [] -> []
  | x::xx, y::yy -> f x y :: map2 f xx yy
  | _ -> raise Map2_length_mismatch
val map2 (#a #b #c: _) (f: (a -> b -> Tac c)) (xs: list a) (ys: list b) : Tac (list c)
let rec map2 #a #b #c (f: (a -> b -> Tac c)) (xs: list a) (ys: list b) : Tac (list c) =
match xs, ys with
| [], [] -> []
| x :: xx, y :: yy -> f x y :: map2 f xx yy
| _ -> raise Map2_length_mismatch
Pulse.Recursion.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.PP.fst.checked prims.fst.checked FStar.Tactics.V2.SyntaxHelpers.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.NamedView.fsti.checked FStar.Stubs.Pprint.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Recursion.fst
Prims.list FStar.Pervasives.Native.Mktuple2 Prims.Nil Prims.Cons Pulse.Recursion.map2 FStar.Pervasives.Native.tuple2 FStar.Tactics.Effect.raise Pulse.Recursion.Map2_length_mismatch
module Pulse.Recursion

module R = FStar.Reflection.V2
module RT = FStar.Reflection.Typing
module T = FStar.Tactics.V2
open FStar.Tactics.V2
module RU = Pulse.RuntimeUtils

open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing
module P = Pulse.Syntax.Printer

exception Splitlast_empty

let rec splitlast #a (l : list a) : Tac (list a & a) =
  match l with
  | [] -> raise Splitlast_empty
  | [x] -> [], x
  | x::xs ->
    let init, last = splitlast xs in
    x::init, last

 exception Map2_length_mismatch
val map2 (#a #b #c: _) (f: (a -> b -> Tac c)) (xs: list a) (ys: list b) : Tac (list c)
f: (_: a -> _: b -> FStar.Tactics.Effect.Tac c) -> xs: Prims.list a -> ys: Prims.list b
  -> FStar.Tactics.Effect.Tac (Prims.list c)