val _split_subst_at_bv (#a #b: Type) (x: bv) (subst: list ((bv & a) & b))
    : Tot (list ((bv & a) & b) & list ((bv & a) & b)) (decreases subst)
let rec _split_subst_at_bv (#a #b : Type) (x : bv) (subst : list ((bv & a) & b)) :
  Tot (list ((bv & a) & b) & list ((bv & a) & b))
  (decreases subst) =
  match subst with
  | [] -> [], []
  | ((src, ty), tgt) :: subst' ->
    if bv_eq x src then
      [], subst'
    else 
      let s1, s2 = _split_subst_at_bv x subst' in
      ((src, ty), tgt) :: s1, s2
val _split_subst_at_bv (#a #b: Type) (x: bv) (subst: list ((bv & a) & b))
    : Tot (list ((bv & a) & b) & list ((bv & a) & b)) (decreases subst)
let rec _split_subst_at_bv (#a #b: Type) (x: bv) (subst: list ((bv & a) & b))
    : Tot (list ((bv & a) & b) & list ((bv & a) & b)) (decreases subst) =
match subst with
| [] -> [], []
| ((src, ty), tgt) :: subst' ->
  if bv_eq x src
  then [], subst'
  else
    let s1, s2 = _split_subst_at_bv x subst' in
    ((src, ty), tgt) :: s1, s2
FStar.InteractiveHelpers.Output.fst.checked
prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.InteractiveHelpers.Propositions.fst.checked FStar.InteractiveHelpers.ExploreTerm.fst.checked FStar.InteractiveHelpers.Base.fst.checked
FStar.InteractiveHelpers.Output.fst
FStar.Reflection.Types.bv Prims.list FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 Prims.Nil FStar.InteractiveHelpers.Base.bv_eq Prims.bool Prims.Cons FStar.InteractiveHelpers.Output._split_subst_at_bv
module FStar.InteractiveHelpers.Output

open FStar.List
open FStar.Tactics
open FStar.Mul
open FStar.InteractiveHelpers.Base
open FStar.InteractiveHelpers.ExploreTerm
open FStar.InteractiveHelpers.Propositions

/// Facilities to output results to the IDE/emacs/whatever.
/// Contains datatypes and functions to carry information.

#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"

(*** Convert terms to string *)
/// The important point is to handle variable shadowing properly, so that the
/// generated term is meaningful in the user context, or at least that it is clear
/// to the user that some variables are shadowed.

/// Introduce fresh variables for the variables shadowed in the current environment
/// and substitute them in the terms. Note that as the binding of the value returned
/// by a function application might shadow one of its parameters, we need to treat
/// differently the pre-assertions and the post-assertions. Moreover, we need to
/// keep track of which variables are shadowed for every assertion.
  
let rec _split_subst_at_bv (#a #b : Type) (x : bv) (subst : list ((bv & a) & b)) :
  Tot (list ((bv & a) & b) & list ((bv & a) & b))
val _split_subst_at_bv (#a #b: Type) (x: bv) (subst: list ((bv & a) & b))
    : Tot (list ((bv & a) & b) & list ((bv & a) & b)) (decreases subst)
x: FStar.Reflection.Types.bv -> subst: Prims.list ((FStar.Reflection.Types.bv * a) * b)
  -> Prims.Tot
    (Prims.list ((FStar.Reflection.Types.bv * a) * b) *
      Prims.list ((FStar.Reflection.Types.bv * a) * b))