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
Library
Module
Module type
Parameter
Class
Class type
val name_of_bv : FStar_Reflection_Types.bv -> Prims.stringval type_of_bv : FStar_Reflection_Types.bv -> FStar_Reflection_Types.typval bv_to_string : FStar_Reflection_Types.bv -> Prims.stringval bv_of_binder : FStar_Reflection_Types.binder -> FStar_Reflection_Types.bvval mk_binder : FStar_Reflection_Types.bv -> FStar_Reflection_Types.binderval mk_implicit_binder :
FStar_Reflection_Types.bv ->
FStar_Reflection_Types.binderval name_of_binder : FStar_Reflection_Types.binder -> Prims.stringval type_of_binder :
FStar_Reflection_Types.binder ->
FStar_Reflection_Types.typval binder_to_string : FStar_Reflection_Types.binder -> Prims.stringval flatten_name : FStar_Reflection_Types.name -> Prims.stringval collect_app' :
FStar_Reflection_Data.argv Prims.list ->
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term * FStar_Reflection_Data.argv Prims.listval collect_app :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term * FStar_Reflection_Data.argv Prims.listval mk_e_app :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term Prims.list ->
FStar_Reflection_Types.termval mk_tot_arr_ln :
FStar_Reflection_Types.binder Prims.list ->
FStar_Reflection_Types.term ->
FStar_Reflection_Types.termval collect_arr_ln_bs :
FStar_Reflection_Types.typ ->
FStar_Reflection_Types.binder Prims.list * FStar_Reflection_Types.compval collect_arr_ln :
FStar_Reflection_Types.typ ->
FStar_Reflection_Types.typ Prims.list * FStar_Reflection_Types.compval collect_abs_ln :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.binder Prims.list * FStar_Reflection_Types.termval fv_to_string : FStar_Reflection_Types.fv -> Prims.stringval compare_name :
FStar_Reflection_Types.name ->
FStar_Reflection_Types.name ->
FStar_Order.orderval compare_fv :
FStar_Reflection_Types.fv ->
FStar_Reflection_Types.fv ->
FStar_Order.orderval compare_const :
FStar_Reflection_Data.vconst ->
FStar_Reflection_Data.vconst ->
FStar_Order.orderval compare_binder :
FStar_Reflection_Types.binder ->
FStar_Reflection_Types.binder ->
FStar_Order.orderval compare_term :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term ->
FStar_Order.orderval compare_term_list :
FStar_Reflection_Types.term Prims.list ->
FStar_Reflection_Types.term Prims.list ->
FStar_Order.orderval compare_argv :
FStar_Reflection_Data.argv ->
FStar_Reflection_Data.argv ->
FStar_Order.orderval compare_comp :
FStar_Reflection_Types.comp ->
FStar_Reflection_Types.comp ->
FStar_Order.orderval mk_stringlit : Prims.string -> FStar_Reflection_Types.termval mk_strcat :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term ->
FStar_Reflection_Types.termval mk_cons :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term ->
FStar_Reflection_Types.termval mk_cons_t :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term ->
FStar_Reflection_Types.termval mk_list :
FStar_Reflection_Types.term Prims.list ->
FStar_Reflection_Types.termval mktuple_n :
FStar_Reflection_Types.term Prims.list ->
FStar_Reflection_Types.termval destruct_tuple :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term Prims.list FStar_Pervasives_Native.optionval mkpair :
FStar_Reflection_Types.term ->
FStar_Reflection_Types.term ->
FStar_Reflection_Types.termval head : FStar_Reflection_Types.term -> FStar_Reflection_Types.termval nameof : FStar_Reflection_Types.term -> Prims.stringval is_uvar : FStar_Reflection_Types.term -> Prims.boolval binder_set_qual :
FStar_Reflection_Data.aqualv ->
FStar_Reflection_Types.binder ->
FStar_Reflection_Types.binderval add_check_with :
FStar_VConfig.vconfig ->
FStar_Reflection_Types.sigelt ->
FStar_Reflection_Types.sigelt