fstar 2022.01.15 · OCaml Package

fstar

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

in-package search v0.1.0

package fstar

Legend:
Library
Module
Module type
Parameter
Class
Class type

val pure_effect_qn : Prims.string

val pure_hoare_effect_qn : Prims.string

val stack_effect_qn : Prims.string

val st_effect_qn : Prims.string

val comp_qualifier : 
  FStar_Reflection_Types.comp ->
  FStar_Tactics_Types.proofstate ->
  Prims.string FStar_Tactics_Result.__result

type effect_type =

| E_Total
| E_GTotal
| E_Lemma
| E_PURE
| E_Pure
| E_Stack
| E_ST
| E_Unknown

val uu___is_E_Total : effect_type -> Prims.bool

val uu___is_E_GTotal : effect_type -> Prims.bool

val uu___is_E_Lemma : effect_type -> Prims.bool

val uu___is_E_PURE : effect_type -> Prims.bool

val uu___is_E_Pure : effect_type -> Prims.bool

val uu___is_E_Stack : effect_type -> Prims.bool

val uu___is_E_ST : effect_type -> Prims.bool

val uu___is_E_Unknown : effect_type -> Prims.bool

val effect_type_to_string : effect_type -> Prims.string

val effect_name_to_type : FStar_Reflection_Types.name -> effect_type

val effect_type_is_pure : effect_type -> Prims.bool

type type_info = {

ty : FStar_Reflection_Types.typ;
refin : FStar_Reflection_Types.term FStar_Pervasives_Native.option;

}

val __proj__Mktype_info__item__ty : type_info -> FStar_Reflection_Types.typ

val __proj__Mktype_info__item__refin : 
  type_info ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option

val mk_type_info : 
  FStar_Reflection_Types.typ ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  type_info

val type_info_to_string : type_info -> Prims.string

val unit_type_info : type_info

val safe_tc : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option
    FStar_Tactics_Result.__result

val safe_tcc : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.comp FStar_Pervasives_Native.option
    FStar_Tactics_Result.__result

val get_type_info_from_type : 
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  type_info FStar_Tactics_Result.__result

val get_type_info : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  type_info FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val get_total_or_gtotal_ret_type : 
  FStar_Reflection_Types.comp ->
  FStar_Reflection_Types.typ FStar_Pervasives_Native.option

val get_comp_ret_type : 
  FStar_Reflection_Types.comp ->
  FStar_Reflection_Types.typ

val is_total_or_gtotal : FStar_Reflection_Types.comp -> Prims.bool

val is_unit_type : 
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result

type typ_or_comp =

| TC_Typ of FStar_Reflection_Types.typ * FStar_Reflection_Types.binder Prims.list * Prims.nat
| TC_Comp of FStar_Reflection_Types.comp * FStar_Reflection_Types.binder Prims.list * Prims.nat

val uu___is_TC_Typ : typ_or_comp -> Prims.bool

val __proj__TC_Typ__item__v : typ_or_comp -> FStar_Reflection_Types.typ

val __proj__TC_Typ__item__pl : 
  typ_or_comp ->
  FStar_Reflection_Types.binder Prims.list

val __proj__TC_Typ__item__num_unflushed : typ_or_comp -> Prims.nat

val uu___is_TC_Comp : typ_or_comp -> Prims.bool

val __proj__TC_Comp__item__v : typ_or_comp -> FStar_Reflection_Types.comp

val __proj__TC_Comp__item__pl : 
  typ_or_comp ->
  FStar_Reflection_Types.binder Prims.list

val __proj__TC_Comp__item__num_unflushed : typ_or_comp -> Prims.nat

val typ_or_comp_to_string : typ_or_comp -> Prims.string

val params_of_typ_or_comp : 
  typ_or_comp ->
  FStar_Reflection_Types.binder Prims.list

val num_unflushed_of_typ_or_comp : typ_or_comp -> Prims.nat

val safe_typ_or_comp : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  typ_or_comp FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val subst_bv_in_comp : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.bv ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.comp ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.comp FStar_Tactics_Result.__result

val subst_binder_in_comp : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.binder ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.comp ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.comp FStar_Tactics_Result.__result

val unfold_until_arrow : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.typ FStar_Tactics_Result.__result

val inst_comp_once : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.comp ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.comp FStar_Tactics_Result.__result

val inst_comp : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.comp ->
  FStar_Reflection_Types.term Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.comp FStar_Tactics_Result.__result

val _abs_update_typ : 
  FStar_Reflection_Types.binder ->
  FStar_Reflection_Types.typ ->
  FStar_Reflection_Types.binder Prims.list ->
  FStar_Reflection_Types.env ->
  FStar_Tactics_Types.proofstate ->
  typ_or_comp FStar_Tactics_Result.__result

val abs_update_typ_or_comp : 
  FStar_Reflection_Types.binder ->
  typ_or_comp ->
  FStar_Reflection_Types.env ->
  FStar_Tactics_Types.proofstate ->
  typ_or_comp FStar_Tactics_Result.__result

val abs_update_opt_typ_or_comp : 
  FStar_Reflection_Types.binder ->
  typ_or_comp FStar_Pervasives_Native.option ->
  FStar_Reflection_Types.env ->
  FStar_Tactics_Types.proofstate ->
  typ_or_comp FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val _flush_typ_or_comp_comp : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.binder Prims.list ->
  (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list ->
  FStar_Reflection_Types.comp ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.comp FStar_Tactics_Result.__result

val flush_typ_or_comp : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  typ_or_comp ->
  FStar_Tactics_Types.proofstate ->
  typ_or_comp FStar_Tactics_Result.__result

val safe_arg_typ_or_comp : 
  Prims.bool ->
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  typ_or_comp FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val convert_ctrl_flag : 
  FStar_Tactics_Types.ctrl_flag ->
  FStar_Tactics_Types.ctrl_flag

type !'a explorer =
  'a ->
  FStar_InteractiveHelpers_Base.genv ->
  (FStar_InteractiveHelpers_Base.genv * FStar_Reflection_Data.term_view)
    Prims.list ->
  typ_or_comp FStar_Pervasives_Native.option ->
  FStar_Reflection_Data.term_view ->
  FStar_Tactics_Types.proofstate ->
  ('a * FStar_Tactics_Types.ctrl_flag) FStar_Tactics_Result.__result

val bind_expl : 
  'a ->
  ('a ->
    FStar_Tactics_Types.proofstate ->
    ('a * FStar_Tactics_Types.ctrl_flag) FStar_Tactics_Result.__result) ->
  ('a ->
    FStar_Tactics_Types.proofstate ->
    ('a * FStar_Tactics_Types.ctrl_flag) FStar_Tactics_Result.__result) ->
  FStar_Tactics_Types.proofstate ->
  ('a * FStar_Tactics_Types.ctrl_flag) FStar_Tactics_Result.__result

val explore_term : 
  Prims.bool ->
  Prims.bool ->
  Prims.unit ->
  Obj.t explorer ->
  Obj.t ->
  FStar_InteractiveHelpers_Base.genv ->
  (FStar_InteractiveHelpers_Base.genv * FStar_Reflection_Data.term_view)
    Prims.list ->
  typ_or_comp FStar_Pervasives_Native.option ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  (Obj.t * FStar_Tactics_Types.ctrl_flag) FStar_Tactics_Result.__result

val explore_pattern : 
  Prims.bool ->
  Prims.bool ->
  Prims.unit ->
  Obj.t explorer ->
  Obj.t ->
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Data.pattern ->
  FStar_Tactics_Types.proofstate ->
  (FStar_InteractiveHelpers_Base.genv * Obj.t * FStar_Tactics_Types.ctrl_flag)
    FStar_Tactics_Result.__result

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

val abs_free_in : 
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.bv Prims.list FStar_Tactics_Result.__result

val shadowed_free_in : 
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.bv Prims.list FStar_Tactics_Result.__result

val term_has_shadowed_variables : 
  FStar_InteractiveHelpers_Base.genv ->
  FStar_Reflection_Types.term ->
  FStar_Tactics_Types.proofstate ->
  Prims.bool FStar_Tactics_Result.__result