val refl_abs_binders (t: R.term) (acc: list binder) : T.Tac (list binder)
let rec refl_abs_binders (t:R.term) (acc:list binder) : T.Tac (list binder) =
  let open R in
  match inspect_ln t with
  | Tv_Abs b body ->
    let {sort; ppname} = R.inspect_binder b in
    let sort = option_must (readback_ty sort)
      (Printf.sprintf "Failed to readback elaborated binder sort %s in refl_abs_binders"
         (T.term_to_string sort)) in
    refl_abs_binders body
     ({ binder_ty = sort; binder_ppname = mk_ppname ppname (RU.range_of_term t) }::acc)
  | _ -> L.rev acc
val refl_abs_binders (t: R.term) (acc: list binder) : T.Tac (list binder)
let rec refl_abs_binders (t: R.term) (acc: list binder) : T.Tac (list binder) =
let open R in
match inspect_ln t with
| Tv_Abs b body ->
  let { sort = sort ; ppname = ppname } = R.inspect_binder b in
  let sort =
    option_must (readback_ty sort)
      (Printf.sprintf "Failed to readback elaborated binder sort %s in refl_abs_binders"
          (T.term_to_string sort))
  in
  refl_abs_binders body
    ({ binder_ty = sort; binder_ppname = mk_ppname ppname (RU.range_of_term t) } :: acc)
| _ -> L.rev acc
Pulse.Checker.AssertWithBinders.fst.checked
Pulse.Typing.Env.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.Naming.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Elaborate.Pure.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.Substs.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.Visit.fst.checked FStar.Tactics.V2.fst.checked FStar.String.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Reflection.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.AssertWithBinders.fst
FStar.Reflection.Types.term Prims.list Pulse.Syntax.Base.binder FStar.Reflection.V2.Builtins.inspect_ln FStar.Reflection.Types.binder FStar.Reflection.Types.typ FStar.Reflection.V2.Data.aqualv FStar.Reflection.V2.Data.ppname_t Pulse.Checker.AssertWithBinders.refl_abs_binders Prims.Cons Pulse.Syntax.Base.Mkbinder Pulse.Syntax.Base.mk_ppname Pulse.RuntimeUtils.range_of_term Pulse.Syntax.Base.term Prims.eq2 Pulse.Elaborate.Pure.elab_term Pulse.Checker.AssertWithBinders.option_must Pulse.Readback.readback_ty Prims.string FStar.Printf.sprintf FStar.Tactics.V2.Builtins.term_to_string FStar.Reflection.V2.Data.binder_view Prims.precedes FStar.Reflection.V2.Builtins.inspect_binder FStar.Reflection.V2.Data.term_view FStar.List.Tot.Base.rev
module Pulse.Checker.AssertWithBinders


open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Base
open Pulse.Elaborate.Pure
open Pulse.Typing.Env

module L = FStar.List.Tot
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
module PC = Pulse.Checker.Pure
module P = Pulse.Syntax.Printer
module N = Pulse.Syntax.Naming
module PS = Pulse.Checker.Prover.Substs
module Prover = Pulse.Checker.Prover

module RU = Pulse.RuntimeUtils

let is_host_term (t:R.term) = not (R.Tv_Unknown? (R.inspect_ln t))

let debug_log = Pulse.Typing.debug_log "with_binders"

let option_must (f:option 'a) (msg:string) : T.Tac 'a =
  match f with
  | Some x -> x
  | None -> T.fail msg
val refl_abs_binders (t: R.term) (acc: list binder) : T.Tac (list binder)
t: FStar.Reflection.Types.term -> acc: Prims.list Pulse.Syntax.Base.binder
  -> FStar.Tactics.Effect.Tac (Prims.list Pulse.Syntax.Base.binder)