val apply (t: T.term) : T.Tac unit
let apply (t:T.term) : T.Tac unit =
  T.t_apply true false true t
val apply (t: T.term) : T.Tac unit
let apply (t: T.term) : T.Tac unit =
T.t_apply true false true t
LowParse.SLow.Tac.Enum.fst.checked
prims.fst.checked LowParse.TacLib.fst.checked LowParse.Spec.Tac.Enum.fst.checked LowParse.SLow.Enum.fst.checked FStar.Pervasives.fsti.checked
LowParse.SLow.Tac.Enum.fst
FStar.Reflection.Types.term FStar.Tactics.V1.Builtins.t_apply Prims.unit
module LowParse.SLow.Tac.Enum
include LowParse.Spec.Tac.Enum
include LowParse.SLow.Enum

module T = LowParse.TacLib

//
// The enum tactic solves goals of type ?u:eqtype with enum types that are
//   in the environment at type Type0
// So typechecking such uvars fails since F* 2635 bug fix
//   (since uvar solutions are checked with smt off)
//
// To circumvent that, we use t_apply with tc_resolve_uvars flag on,
//   so that ?u will be typechecked as soon as it is resolved,
//   resulting in an smt guard that will be added to the proofstate
//
val apply (t: T.term) : T.Tac unit
t: FStar.Reflection.Types.term -> FStar.Tactics.Effect.Tac Prims.unit