let end_proof () =
  tadmit_t (`())
let end_proof () =
tadmit_t (`())
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.unit FStar.Tactics.V1.Builtins.tadmit_t
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
val end_proof : _: Prims.unit -> FStar.Tactics.Effect.Tac Prims.unit
_: Prims.unit -> FStar.Tactics.Effect.Tac Prims.unit