To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
package fstar
-
fstarlib
-
fstartaclib
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
module RB = FStar_Reflection_Basicval compare_bv :
FStar_Syntax_Syntax.bv ->
FStar_Syntax_Syntax.bv ->
FStar_Order.orderval lookup_typ :
FStar_TypeChecker_Env.env ->
Prims.string Prims.list ->
FStar_Syntax_Syntax.sigelt FStar_Pervasives_Native.optionval is_free : FStar_Syntax_Syntax.bv -> FStar_Syntax_Syntax.term -> Prims.boolval free_bvs : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.bv Prims.listval free_uvars : FStar_Syntax_Syntax.term -> FStar_BigInt.t Prims.listval lookup_attr :
FStar_Syntax_Syntax.term ->
FStar_TypeChecker_Env.env ->
FStar_Syntax_Syntax.fv Prims.listval all_defs_in_env :
FStar_TypeChecker_Env.env ->
FStar_Syntax_Syntax.fv Prims.listval defs_in_module :
FStar_TypeChecker_Env.env ->
FStar_Reflection_Data.name ->
FStar_Syntax_Syntax.fv Prims.listval binders_of_env : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.bindersval moduleof : FStar_TypeChecker_Env.env -> Prims.string Prims.listval term_eq :
FStar_Syntax_Syntax.term ->
FStar_Syntax_Syntax.term ->
Prims.boolval term_to_string : FStar_Syntax_Syntax.term -> Prims.stringval comp_to_string : FStar_Syntax_Syntax.comp -> Prims.stringval env_open_modules :
FStar_TypeChecker_Env.env ->
FStar_Reflection_Data.name Prims.listval sigelt_opts :
FStar_Syntax_Syntax.sigelt ->
FStar_VConfig.vconfig FStar_Pervasives_Native.optionval embed_vconfig : FStar_VConfig.vconfig -> FStar_Syntax_Syntax.termval sigelt_attrs :
FStar_Syntax_Syntax.sigelt ->
FStar_Syntax_Syntax.attribute Prims.listval set_sigelt_attrs :
FStar_Syntax_Syntax.attribute Prims.list ->
FStar_Syntax_Syntax.sigelt ->
FStar_Syntax_Syntax.sigeltval sigelt_quals :
FStar_Syntax_Syntax.sigelt ->
FStar_Reflection_Data.qualifier Prims.listval set_sigelt_quals :
FStar_Reflection_Data.qualifier Prims.list ->
FStar_Syntax_Syntax.sigelt ->
FStar_Syntax_Syntax.sigeltval inspect_fv : FStar_Syntax_Syntax.fv -> Prims.string Prims.listval pack_fv : Prims.string Prims.list -> FStar_Syntax_Syntax.fvval inspect_const : FStar_Syntax_Syntax.sconst -> FStar_Reflection_Data.vconstval pack_const : FStar_Reflection_Data.vconst -> FStar_Syntax_Syntax.sconstval inspect_ln : FStar_Syntax_Syntax.term -> FStar_Reflection_Data.term_viewval pack_ln : FStar_Reflection_Data.term_view -> FStar_Syntax_Syntax.termval inspect_comp : FStar_Syntax_Syntax.comp -> FStar_Reflection_Data.comp_viewval pack_comp : FStar_Reflection_Data.comp_view -> FStar_Syntax_Syntax.compval inspect_sigelt :
FStar_Syntax_Syntax.sigelt ->
FStar_Reflection_Data.sigelt_viewval pack_sigelt :
FStar_Reflection_Data.sigelt_view ->
FStar_Syntax_Syntax.sigeltval inspect_bv : FStar_Syntax_Syntax.bv -> FStar_Reflection_Data.bv_viewval pack_bv : FStar_Reflection_Data.bv_view -> FStar_Syntax_Syntax.bvval inspect_binder :
FStar_Syntax_Syntax.binder ->
FStar_Syntax_Syntax.bv
* (FStar_Reflection_Data.aqualv * FStar_Syntax_Syntax.term Prims.list)val pack_binder :
FStar_Syntax_Syntax.bv ->
FStar_Reflection_Data.aqualv ->
FStar_Syntax_Syntax.term Prims.list ->
FStar_Syntax_Syntax.binderval inspect_lb :
FStar_Syntax_Syntax.letbinding ->
FStar_Reflection_Data.lb_viewval pack_lb : FStar_Reflection_Data.lb_view -> FStar_Syntax_Syntax.letbindingval implode_qn : Prims.string Prims.list -> Prims.stringval explode_qn : Prims.string -> Prims.string Prims.listval compare_string : Prims.string -> Prims.string -> FStar_BigInt.tval push_binder :
FStar_TypeChecker_Env.env ->
FStar_Syntax_Syntax.binder ->
FStar_TypeChecker_Env.envval subst :
FStar_Syntax_Syntax.bv ->
FStar_Syntax_Syntax.term ->
FStar_Syntax_Syntax.term ->
FStar_Syntax_Syntax.termval close_term :
FStar_Syntax_Syntax.binder ->
FStar_Syntax_Syntax.term ->
FStar_Syntax_Syntax.termval inspect_aqual : FStar_Syntax_Syntax.aqual -> FStar_Reflection_Data.aqualvval pack_aqual : FStar_Reflection_Data.aqualv -> FStar_Syntax_Syntax.aqual