fstar 2022.01.15 · OCaml Package

To focus the search input from anywhere on the page, press the 'S' key.

in-package search v0.1.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

exception Goal_not_trivial

val uu___is_Goal_not_trivial : Prims.exn -> Prims.bool

val goals : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Tactics_Types.goal Prims.list FStar_Tactics_Result.__result

val smt_goals : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Tactics_Types.goal Prims.list FStar_Tactics_Result.__result

val fail : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val fail_silently : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val _cur_goal : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Tactics_Types.goal FStar_Tactics_Result.__result

val cur_env : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.env FStar_Tactics_Result.__result

val cur_goal : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.typ FStar_Tactics_Result.__result

val cur_witness : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val cur_goal_safe : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Tactics_Types.goal FStar_Tactics_Result.__result

val cur_binders : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binders FStar_Tactics_Result.__result

val with_policy : 
  FStar_Tactics_Types.guard_policy ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val exact : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val exact_with_ref : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val trivial : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val dismiss : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val flip : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val qed : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val debug : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val smt : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val idtac : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val later : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val apply : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val apply_noinst : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val apply_lemma : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val trefl : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val trefl_guard : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val commute_applied_match : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val apply_lemma_noinst : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val apply_lemma_rw : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val apply_raw : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val exact_guard : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val t_pointwise : 
  FStar_Tactics_Types.direction ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val topdown_rewrite : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    (Prims.bool * Prims.int) FStar_Tactics_Result.__result) ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val pointwise : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val pointwise' : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val cur_module : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.name FStar_Tactics_Result.__result

val open_modules : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.name Prims.list FStar_Tactics_Result.__result

val repeatn : 
  Prims.int ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a Prims.list FStar_Tactics_Result.__result

val fresh_uvar : 
  FStar_Reflection_Types.typ FStar_Pervasives_Native.option ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val unify : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val unify_guard : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val tmatch : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val divide : 
  Prims.int ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'b FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  ('a * 'b) FStar_Tactics_Result.__result

val iseq : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result)
    Prims.list ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val focus : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val dump1 : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val mapAll : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a Prims.list FStar_Tactics_Result.__result

val iterAll : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val iterAllSMT : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val seq : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val exact_args : 
  FStar_Reflection_Data.aqualv Prims.list ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val exact_n : 
  Prims.int ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val ngoals : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.int FStar_Tactics_Result.__result

val ngoals_smt : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.int FStar_Tactics_Result.__result

val fresh_bv : 
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.bv FStar_Tactics_Result.__result

val fresh_binder_named : 
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val fresh_binder : 
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val fresh_implicit_binder_named : 
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val fresh_implicit_binder : 
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val guard : 
  Prims.bool ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val try_with : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  (Prims.exn ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val trytac : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val or_else : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val op_Less_Bar_Greater : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val first : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result)
    Prims.list ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val repeat : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a Prims.list FStar_Tactics_Result.__result

val repeat1 : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a Prims.list FStar_Tactics_Result.__result

val repeat' : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val norm_term : 
  FStar_Pervasives.norm_step Prims.list ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val join_all_smt_goals : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val discard : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val repeatseq : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val tadmit : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val admit1 : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val admit_all : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val is_guard : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val skip_guard : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val guards_to_smt : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val simpl : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val whnf : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val compute : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val intros : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder Prims.list FStar_Tactics_Result.__result

val intros' : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val destruct : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val destruct_intros : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val __cut : ('a -> 'b) -> 'a -> 'b

val tcut : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val pose : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val intro_as : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val pose_as : 
  Prims.string ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val for_each_binder : 
  (FStar_Reflection_Types.binder ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a Prims.list FStar_Tactics_Result.__result

val revert_all : 
  FStar_Reflection_Types.binders ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val bv_to_term : 
  FStar_Reflection_Types.bv ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val binder_to_term : 
  FStar_Reflection_Types.binder ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val __assumption_aux : 
  FStar_Reflection_Types.binders ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val assumption : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val destruct_equality_implication : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Formula.formula * FStar_Reflection_Types.term)
    FStar_Pervasives_Native.option
    FStar_Tactics_Result.__result

val rewrite' : 
  FStar_Reflection_Types.binder ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val try_rewrite_equality : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.binders ->
  Prims.unit FStar_Tactics_Effect.__tac

val rewrite_all_context_equalities : 
  FStar_Reflection_Types.binders ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val rewrite_eqs_from_context : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val rewrite_equality : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val unfold_def : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val l_to_r : 
  FStar_Reflection_Types.term Prims.list ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val mk_squash : FStar_Reflection_Types.term -> FStar_Reflection_Types.term

val mk_sq_eq : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term

val grewrite : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val grewrite_eq : 
  FStar_Reflection_Types.binder ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val apply_squash_or_lem : 
  Prims.nat ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val mapply : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val admit_dump_t : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val admit_dump : (Prims.unit -> 'a) -> Prims.unit -> 'a

val magic_dump_t : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val magic_dump : 'a -> Prims.unit -> 'a

val change_with : 
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val change_sq : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val finish_by : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val solve_then : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  ('a -> FStar_Tactics_Types.proofstate -> 'b FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'b FStar_Tactics_Result.__result

val add_elem : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    'a FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val specialize : 
  'a ->
  Prims.string Prims.list ->
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val tlabel : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val tlabel' : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val focus_all : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val extract_nth : 
  Prims.nat ->
  'a Prims.list ->
  ('a * 'a Prims.list) FStar_Pervasives_Native.option

val bump_nth : 
  Prims.pos ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val on_sort_bv : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  FStar_Reflection_Types.bv ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.bv FStar_Tactics_Result.__result

val on_sort_binder : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  FStar_Reflection_Types.binder ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

val visit_tm : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val visit_br : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  FStar_Reflection_Data.branch ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Data.branch FStar_Tactics_Result.__result

val visit_pat : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  FStar_Reflection_Data.pattern ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Data.pattern FStar_Tactics_Result.__result

val visit_comp : 
  (FStar_Reflection_Types.term ->
    FStar_Tactics_Types.proofstate ->
    FStar_Reflection_Types.term FStar_Tactics_Result.__result) ->
  FStar_Reflection_Types.comp ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.comp FStar_Tactics_Result.__result

val destruct_list : 
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term Prims.list FStar_Tactics_Result.__result

val get_match_body : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val last : 
  'a Prims.list ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val branch_on_match : 
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  Prims.unit FStar_Tactics_Result.__result

val nth_binder : 
  Prims.int ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.binder FStar_Tactics_Result.__result

exception Appears

val uu___is_Appears : Prims.exn -> Prims.bool

val name_appears_in : 
  FStar_Reflection_Types.name ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

val mk_abs : 
  FStar_Reflection_Types.binder Prims.list ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result