val is_focus_on_term : term -> Tac bool
let is_focus_on_term t = is_fvar t (`%focus_on_term)
val is_focus_on_term : term -> Tac bool
let is_focus_on_term t =
is_fvar t (`%focus_on_term)
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
FStar.Reflection.Types.term FStar.Reflection.V1.Derived.is_fvar Prims.bool
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)
               (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
#pop-options

/// This function goes through the goal, which is presumed to be a squashed equality,
/// and prints all the subterms of its left operand. Very useful for debugging.
val pp_explore_print_goal : unit -> Tac unit
let pp_explore_print_goal () =
  let f : explorer unit =
    fun _ _ _ _ _ -> ((), Continue)
  in
  pp_explore true false f ()

/// Check for meta-identifiers. Note that we can't simply use ``term_eq`` which
/// sometimes unexpectedly fails (maybe because of information hidden to Meta-F*)
val is_focus_on_term : term -> Tac bool
t: FStar.Reflection.Types.term -> FStar.Tactics.Effect.Tac Prims.bool