val collect_arr' (bs: list binder) (c: comp) : Tac (list binder * comp)
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: list binder) (c: comp) : Tac (list binder * comp)
let rec collect_arr' (bs: list binder) (c: comp) : Tac (list binder * comp) =
match c with
| C_Total t ->
  (match inspect t with
    | Tv_Arrow b c -> collect_arr' (b :: bs) c
    | _ -> (bs, c))
| _ -> (bs, 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
Prims.list FStar.Tactics.NamedView.binder FStar.Tactics.NamedView.comp FStar.Reflection.Types.typ FStar.Tactics.V2.SyntaxHelpers.collect_arr' Prims.Cons FStar.Pervasives.Native.tuple2 FStar.Tactics.NamedView.named_term_view FStar.Pervasives.Native.Mktuple2 FStar.Tactics.NamedView.inspect FStar.Reflection.V2.Data.comp_view
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
val collect_arr' (bs: list binder) (c: comp) : Tac (list binder * comp)
bs: Prims.list FStar.Tactics.NamedView.binder -> c: FStar.Tactics.NamedView.comp
  -> FStar.Tactics.Effect.Tac
    (Prims.list FStar.Tactics.NamedView.binder * FStar.Tactics.NamedView.comp)