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

type !'a __tac =
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val __ret : 'a -> 'a __tac

val __bind : 
  Prims.range ->
  Prims.range ->
  'a __tac ->
  ('a -> 'b __tac) ->
  'b __tac

val __get : Prims.unit -> FStar_Tactics_Types.proofstate __tac

val __raise : Prims.exn -> 'a __tac

type 'a __tac_wp = Prims.unit

type ('a, 'b, !'wp, 'f, 'ps, 'post) g_bind = 'wp

type ('a, 'wp, 'ps, 'post) g_compact = Prims.unit

type ('a, 'b, 'wp, 'f, 'uuuuu, 'uuuuu1) __TAC_eff_override_bind_wp = Prims.unit

type ('a, !'wp, 's, 'pu) _dm4f_TAC_lift_from_pure = 'wp

type ('a, 'x, 's, !'pu) _dm4f_TAC_return_wp = 'pu

val _dm4f_TAC_return_elab : 
  'a ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

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

val _dm4f_TAC___proj__TAC__item____raise_elab : 
  Prims.exn ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

type _dm4f_TAC___proj__TAC__item____raise_complete_type =
  Prims.unit ->
  Prims.exn ->
  FStar_Tactics_Types.proofstate ->
  Obj.t FStar_Tactics_Result.__result

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

type _dm4f_TAC___proj__TAC__item____get_complete_type =
  Prims.unit ->
  FStar_Tactics_Types.proofstate ->
  FStar_Tactics_Types.proofstate FStar_Tactics_Result.__result

type (!'a, 'wpua) _dm4f_TAC_repr =
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

type _dm4f_TAC_pre = Prims.unit

type 'a _dm4f_TAC_post = Prims.unit

type 'a _dm4f_TAC_wp = Prims.unit

type ('a, !'t) _dm4f_TAC_ctx =
  FStar_Tactics_Types.proofstate ->
  Prims.unit ->
  't

type ('a, 't) _dm4f_TAC_gctx = Prims.unit

val _dm4f_TAC_pure : 't -> FStar_Tactics_Types.proofstate -> Prims.unit -> 't

type ('a, 'c, 'uuuuu, 'uuuuu1, 'uuuuu2, 'uuuuu3) _dm4f_TAC_wp_if_then_else =
  Prims.unit

type ('a, 'b, 'f, 'uuuuu, 'uuuuu1) _dm4f_TAC_wp_close = Prims.unit

type ('a, 'wp1, 'wp2) _dm4f_TAC_stronger = Prims.unit

type ('a, 'wp, 'uuuuu, 'uuuuu1) _dm4f_TAC_ite_wp = Prims.unit

type ('a, 'uuuuu, 'uuuuu1) _dm4f_TAC_null_wp = Prims.unit

type ('a, 'wp) _dm4f_TAC_wp_trivial = Prims.unit

val __proj__TAC__item__return : 
  'a ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

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

val __proj__TAC__item____raise : 
  Prims.exn ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

val __proj__TAC__item____get : 
  'a ->
  FStar_Tactics_Types.proofstate ->
  FStar_Tactics_Types.proofstate FStar_Tactics_Result.__result

type ('a, !'wp, 'ps, 'p) lift_div_tac = 'wp

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

val raise : 
  Prims.exn ->
  FStar_Tactics_Types.proofstate ->
  'a FStar_Tactics_Result.__result

type ('uuuuu, !'p) with_tactic = 'p

val rewrite_with_tactic : 
  (Prims.unit ->
    FStar_Tactics_Types.proofstate ->
    Prims.unit FStar_Tactics_Result.__result) ->
  Prims.unit ->
  Obj.t ->
  Obj.t

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

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

type (!'a, !'b) tac =
  'a ->
  FStar_Tactics_Types.proofstate ->
  'b FStar_Tactics_Result.__result

type !'a tactic = (Prims.unit, 'a) tac