val splitlast (#a: _) (l: list a) : Tac (list a & a)
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
val splitlast (#a: _) (l: list a) : Tac (list a & a)
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
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.Tactics.Effect.raise FStar.Pervasives.Native.tuple2 Pulse.Recursion.Splitlast_empty FStar.Pervasives.Native.Mktuple2 Prims.Nil Prims.Cons Pulse.Recursion.splitlast
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
val splitlast (#a: _) (l: list a) : Tac (list a & a)
l: Prims.list a -> FStar.Tactics.Effect.Tac (Prims.list a * a)