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

val bv_eq : 
  FStar_Reflection_Types.bv ->
  FStar_Reflection_Types.bv ->
  Prims.bool

val fv_eq : 
  FStar_Reflection_Types.fv ->
  FStar_Reflection_Types.fv ->
  Prims.bool

val fv_eq_name : 
  FStar_Reflection_Types.fv ->
  FStar_Reflection_Types.name ->
  Prims.bool

val opt_apply : 
  ('a -> 'b) ->
  'a FStar_Pervasives_Native.option ->
  'b FStar_Pervasives_Native.option

val opt_tapply : 
  ('a -> FStar_Tactics_Types.proofstate -> 'b FStar_Tactics_Result.__result) ->
  'a FStar_Pervasives_Native.option ->
  FStar_Tactics_Types.proofstate ->
  'b FStar_Pervasives_Native.option FStar_Tactics_Result.__result

val option_to_string : 
  ('a -> Prims.string) ->
  'a FStar_Pervasives_Native.option ->
  Prims.string

val opt_cons : 
  'a FStar_Pervasives_Native.option ->
  'a Prims.list ->
  'a Prims.list

val list_to_string : ('a -> Prims.string) -> 'a Prims.list -> Prims.string

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

val opt_mk_app_norm : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Reflection_Types.term Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option
    FStar_Tactics_Result.__result

val unzip : ('a * 'b) Prims.list -> 'a Prims.list * 'b Prims.list

val abv_to_string : FStar_Reflection_Types.bv -> Prims.string

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

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

val acomp_to_string : FStar_Reflection_Types.comp -> Prims.string

exception MetaAnalysis of Prims.string

val uu___is_MetaAnalysis : Prims.exn -> Prims.bool

val __proj__MetaAnalysis__item__uu___ : Prims.exn -> Prims.string

val mfail : 
  Prims.string ->
  FStar_Tactics_Types.proofstate ->
  'uuuuu FStar_Tactics_Result.__result

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

val term_view_construct : 
  FStar_Reflection_Data.term_view ->
  FStar_Tactics_Types.proofstate ->
  Prims.string FStar_Tactics_Result.__result

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

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

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

type !'a bind_map = (FStar_Reflection_Types.bv * 'a) Prims.list

val bind_map_push : 
  'a bind_map ->
  FStar_Reflection_Types.bv ->
  'a ->
  (FStar_Reflection_Types.bv * 'a) Prims.list

val bind_map_get : 
  'a bind_map ->
  FStar_Reflection_Types.bv ->
  'a FStar_Pervasives_Native.option

val bind_map_get_from_name : 
  'a bind_map ->
  Prims.string ->
  (FStar_Reflection_Types.bv * 'a) FStar_Pervasives_Native.option

type genv = {

env : FStar_Reflection_Types.env;
bmap : (Prims.bool * FStar_Reflection_Types.term) bind_map;
svars : FStar_Reflection_Types.bv Prims.list;

}

val __proj__Mkgenv__item__env : genv -> FStar_Reflection_Types.env

val __proj__Mkgenv__item__bmap : 
  genv ->
  (Prims.bool * FStar_Reflection_Types.term) bind_map

val __proj__Mkgenv__item__svars : genv -> FStar_Reflection_Types.bv Prims.list

val get_env : genv -> FStar_Reflection_Types.env

val get_bind_map : genv -> (Prims.bool * FStar_Reflection_Types.term) bind_map

val mk_genv : 
  FStar_Reflection_Types.env ->
  (Prims.bool * FStar_Reflection_Types.term) bind_map ->
  FStar_Reflection_Types.bv Prims.list ->
  genv

val mk_init_genv : FStar_Reflection_Types.env -> genv

val genv_to_string : genv -> Prims.string

val genv_get : 
  genv ->
  FStar_Reflection_Types.bv ->
  (Prims.bool * FStar_Reflection_Types.term) FStar_Pervasives_Native.option

val genv_get_from_name : 
  genv ->
  Prims.string ->
  (FStar_Reflection_Types.bv * (Prims.bool * FStar_Reflection_Types.term))
    FStar_Pervasives_Native.option

val genv_push_bv : 
  genv ->
  FStar_Reflection_Types.bv ->
  Prims.bool ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Tactics_Types.proofstate ->
  genv FStar_Tactics_Result.__result

val genv_push_binder : 
  genv ->
  FStar_Reflection_Types.binder ->
  Prims.bool ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  FStar_Tactics_Types.proofstate ->
  genv FStar_Tactics_Result.__result

val bv_is_shadowed : genv -> FStar_Reflection_Types.bv -> Prims.bool

val binder_is_shadowed : genv -> FStar_Reflection_Types.binder -> Prims.bool

val find_shadowed_bvs : 
  genv ->
  FStar_Reflection_Types.bv Prims.list ->
  (FStar_Reflection_Types.bv * Prims.bool) Prims.list

val find_shadowed_binders : 
  genv ->
  FStar_Reflection_Types.binder Prims.list ->
  (FStar_Reflection_Types.binder * Prims.bool) Prims.list

val bv_is_abstract : genv -> FStar_Reflection_Types.bv -> Prims.bool

val binder_is_abstract : genv -> FStar_Reflection_Types.binder -> Prims.bool

val genv_abstract_bvs : genv -> FStar_Reflection_Types.bv Prims.list

val _fresh_bv : 
  Prims.string Prims.list ->
  Prims.string ->
  Prims.int ->
  FStar_Reflection_Types.typ ->
  FStar_Reflection_Types.bv FStar_Tactics_Effect.__tac

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

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

val genv_push_fresh_binder : 
  genv ->
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  (genv * FStar_Reflection_Types.binder) FStar_Tactics_Result.__result

val push_fresh_binder : 
  FStar_Reflection_Types.env ->
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.env * FStar_Reflection_Types.binder)
    FStar_Tactics_Result.__result

val genv_push_fresh_bv : 
  genv ->
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  (genv * FStar_Reflection_Types.bv) FStar_Tactics_Result.__result

val push_fresh_var : 
  FStar_Reflection_Types.env ->
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term
   * FStar_Reflection_Types.binder
   * FStar_Reflection_Types.env)
    FStar_Tactics_Result.__result

val genv_push_fresh_var : 
  genv ->
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term * FStar_Reflection_Types.binder * genv)
    FStar_Tactics_Result.__result

val push_two_fresh_vars : 
  FStar_Reflection_Types.env ->
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term
   * FStar_Reflection_Types.binder
   * FStar_Reflection_Types.term
   * FStar_Reflection_Types.binder
   * FStar_Reflection_Types.env)
    FStar_Tactics_Result.__result

val genv_push_two_fresh_vars : 
  genv ->
  Prims.string ->
  FStar_Reflection_Types.typ ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.term
   * FStar_Reflection_Types.binder
   * FStar_Reflection_Types.term
   * FStar_Reflection_Types.binder
   * genv)
    FStar_Tactics_Result.__result

val norm_apply_subst : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

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

val deep_apply_subst : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

val deep_apply_subst_in_bv : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.bv ->
  (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Types.bv
   * (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list)
    FStar_Tactics_Result.__result

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

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

val deep_apply_subst_in_pattern : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Data.pattern ->
  (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list ->
  FStar_Tactics_Types.proofstate ->
  (FStar_Reflection_Data.pattern
   * (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list)
    FStar_Tactics_Result.__result

val apply_subst : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term ->
  (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Tactics_Result.__result

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

val opt_apply_subst : 
  FStar_Reflection_Types.env ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option ->
  (FStar_Reflection_Types.bv * FStar_Reflection_Types.term) Prims.list ->
  FStar_Tactics_Types.proofstate ->
  FStar_Reflection_Types.term FStar_Pervasives_Native.option
    FStar_Tactics_Result.__result

val _generate_shadowed_subst : 
  genv ->
  FStar_Reflection_Types.term ->
  FStar_Reflection_Types.bv Prims.list ->
  FStar_Tactics_Types.proofstate ->
  (genv * (FStar_Reflection_Types.bv * FStar_Reflection_Types.bv) Prims.list)
    FStar_Tactics_Result.__result

val generate_shadowed_subst : 
  genv ->
  FStar_Tactics_Types.proofstate ->
  (genv * (FStar_Reflection_Types.bv * FStar_Reflection_Types.bv) Prims.list)
    FStar_Tactics_Result.__result