let fail (#a:Type) (m:string) = raise #a (TacticFailure m)
let fail (#a: Type) (m: string) =
raise #a (TacticFailure m)
FStar.Tactics.V2.SyntaxHelpers.fst.checked
prims.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.Types.fsti.checked FStar.Tactics.NamedView.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked
FStar.Tactics.V2.SyntaxHelpers.fst
Prims.string FStar.Tactics.Effect.raise FStar.Tactics.Common.TacticFailure
module FStar.Tactics.V2.SyntaxHelpers

open FStar.Reflection.V2
open FStar.Tactics.Effect
open FStar.Tactics.V2.Builtins
open FStar.Tactics.Types
open FStar.Tactics.NamedView

(* These are fully-named variants of functions found in FStar.Reflection *)

private
let rec collect_arr' (bs : list binder) (c : comp) : Tac (list binder * comp) =
    begin match c with
    | C_Total t ->
        begin match inspect t with
        | Tv_Arrow b c ->
            collect_arr' (b::bs) c
        | _ ->
            (bs, c)
        end
    | _ -> (bs, c)
    end

val collect_arr_bs : typ -> Tac (list binder * comp)
let collect_arr_bs t =
    let (bs, c) = collect_arr' [] (C_Total t) in
    (List.Tot.Base.rev bs, c)

val collect_arr : typ -> Tac (list typ * comp)
let collect_arr t =
    let (bs, c) = collect_arr' [] (C_Total t) in
    let ts = List.Tot.Base.map (fun (b:binder) -> b.sort) bs in
    (List.Tot.Base.rev ts, c)

private
let rec collect_abs' (bs : list binder) (t : term) : Tac (list binder * term) (decreases t) =
    match inspect t with
    | Tv_Abs b t' ->
        collect_abs' (b::bs) t'
    | _ -> (bs, t)

val collect_abs : term -> Tac (list binder * term)
let collect_abs t =
    let (bs, t') = collect_abs' [] t in
    (List.Tot.Base.rev bs, t')

(* Copied from FStar.Tactics.V2.Derived *)
val fail : m: Prims.string -> FStar.Tactics.Effect.Tac a
m: Prims.string -> FStar.Tactics.Effect.Tac a