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)
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)
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
FStar.Reflection.Types.typ Prims.list FStar.Tactics.NamedView.binder FStar.Tactics.NamedView.comp FStar.Pervasives.Native.Mktuple2 FStar.List.Tot.Base.rev FStar.List.Tot.Base.map FStar.Tactics.NamedView.__proj__Mkbinder__item__sort FStar.Pervasives.Native.tuple2 FStar.Tactics.V2.SyntaxHelpers.collect_arr' Prims.Nil FStar.Reflection.V2.Data.C_Total
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)
t: FStar.Reflection.Types.typ
  -> FStar.Tactics.Effect.Tac (Prims.list FStar.Reflection.Types.typ * FStar.Tactics.NamedView.comp)