val check_equiv_now : g:env -> t1:term -> t2:term ->
  Tac (option (equiv_token g t1 t2) & issues)
let check_equiv_now tcenv t0 t1 =
  T.with_policy SMTSync (fun () ->
    T.check_equiv tcenv t0 t1)
val check_equiv_now : g:env -> t1:term -> t2:term ->
  Tac (option (equiv_token g t1 t2) & issues)
let check_equiv_now tcenv t0 t1 =
T.with_policy SMTSync (fun () -> T.check_equiv tcenv t0 t1)
Pulse.Typing.Util.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Typing.Util.fst
FStar.Reflection.Types.env FStar.Tactics.NamedView.term FStar.Tactics.V2.Derived.with_policy FStar.Tactics.V2.Builtins.ret_t FStar.Tactics.Types.equiv_token FStar.Tactics.Types.SMTSync Prims.unit FStar.Tactics.V2.Builtins.check_equiv FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.option FStar.Tactics.Types.issues
module Pulse.Typing.Util

module L = FStar.List.Tot
module T = FStar.Tactics.V2

(* Call check_equiv under a SMTSync guard policy *)
val check_equiv_now : g:env -> t1:term -> t2:term ->
  Tac (option (equiv_token g t1 t2) & issues)

    g: FStar.Reflection.Types.env ->
    t1: FStar.Tactics.NamedView.term ->
    t2: FStar.Tactics.NamedView.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (FStar.Tactics.Types.equiv_token g t1 t2) *
      FStar.Tactics.Types.issues)