val pp_explore (dbg dfs: bool) (#a: Type0) (f: explorer a) (x: a) : Tac unit
let pp_explore (dbg dfs : bool)
               (#a : Type0)
               (f : explorer a)
               (x : a) :
  Tac unit =
  let g = cur_goal () in
  let e = cur_env () in
  print_dbg dbg ("[> pp_explore:\n" ^ term_to_string g);
  begin match unsquash_equality g with
  | Some (l, _) ->
    let c = safe_typ_or_comp dbg e l in
    let ge = mk_genv e [] [] in
    print_dbg dbg ("[> About to explore term:\n" ^ term_to_string l);
    let x = explore_term dbg dfs #a f x ge [] c l in
    end_proof ()
  | _ -> mfail "pp_explore: not a squashed equality"
  end
val pp_explore (dbg dfs: bool) (#a: Type0) (f: explorer a) (x: a) : Tac unit
let pp_explore (dbg dfs: bool) (#a: Type0) (f: explorer a) (x: a) : Tac unit =
let g = cur_goal () in
let e = cur_env () in
print_dbg dbg ("[> pp_explore:\n" ^ term_to_string g);
match unsquash_equality g with
| Some (l, _) ->
  let c = safe_typ_or_comp dbg e l in
  let ge = mk_genv e [] [] in
  print_dbg dbg ("[> About to explore term:\n" ^ term_to_string l);
  let x = explore_term dbg dfs #a f x ge [] c l in
  end_proof ()
| _ -> mfail "pp_explore: not a squashed equality"
FStar.InteractiveHelpers.PostProcess.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.Output.fst.checked FStar.InteractiveHelpers.ExploreTerm.fst.checked FStar.InteractiveHelpers.Effectful.fst.checked FStar.InteractiveHelpers.Base.fst.checked
FStar.InteractiveHelpers.PostProcess.fst
Prims.bool FStar.InteractiveHelpers.ExploreTerm.explorer FStar.Reflection.Types.term FStar.InteractiveHelpers.PostProcess.end_proof Prims.unit FStar.Pervasives.Native.tuple2 FStar.Tactics.Types.ctrl_flag FStar.InteractiveHelpers.ExploreTerm.explore_term Prims.Nil FStar.InteractiveHelpers.Base.genv FStar.Reflection.V1.Data.term_view FStar.InteractiveHelpers.Base.print_dbg Prims.string Prims.op_Hat FStar.Tactics.V1.Builtins.term_to_string FStar.InteractiveHelpers.Base.mk_genv FStar.Reflection.Types.bv FStar.Pervasives.Native.tuple3 FStar.Reflection.Types.typ FStar.Pervasives.Native.option FStar.InteractiveHelpers.ExploreTerm.typ_or_comp Prims.l_imp Prims.b2t FStar.Pervasives.Native.uu___is_Some FStar.InteractiveHelpers.ExploreTerm.uu___is_TC_Comp FStar.Pervasives.Native.__proj__Some__item__v FStar.InteractiveHelpers.ExploreTerm.safe_typ_or_comp FStar.InteractiveHelpers.Base.mfail FStar.InteractiveHelpers.PostProcess.unsquash_equality FStar.Reflection.Types.env FStar.Tactics.V1.Derived.cur_env FStar.Tactics.V1.Derived.cur_goal
module FStar.InteractiveHelpers.PostProcess

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

let term_eq = FStar.Tactics.term_eq_old

/// The high-level post-processing tactics, used to retrieve some specific
/// information from the context and generate output which can be exploited
/// on the IDE side.

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

(*** General utilities *)
/// We declare some identifiers that we will use to guide the meta processing
assume type meta_info
assume val focus_on_term : meta_info

let end_proof () =
  tadmit_t (`())

let unsquash_equality (t:term) : Tac (option (term & term)) =
  begin match term_as_formula t with
  | Comp (Eq _) l r -> Some (l, r)
  | _ -> None
  end

#push-options "--ifuel 2"
let pp_explore (dbg dfs : bool)
               (#a : Type0)
               (f : explorer a)
val pp_explore (dbg dfs: bool) (#a: Type0) (f: explorer a) (x: a) : Tac unit
dbg: Prims.bool -> dfs: Prims.bool -> f: FStar.InteractiveHelpers.ExploreTerm.explorer a -> x: a
  -> FStar.Tactics.Effect.Tac Prims.unit