fstar
  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type varname = Prims.string
type qn = Prims.string
type pattern =
  1. | PAny
  2. | PVar of varname
  3. | PQn of qn
  4. | PType
  5. | PApp of pattern * pattern
val uu___is_PAny : pattern -> Prims.bool
val uu___is_PVar : pattern -> Prims.bool
val __proj__PVar__item__name : pattern -> varname
val uu___is_PQn : pattern -> Prims.bool
val __proj__PQn__item__qn : pattern -> qn
val uu___is_PType : pattern -> Prims.bool
val uu___is_PApp : pattern -> Prims.bool
val __proj__PApp__item__hd : pattern -> pattern
val __proj__PApp__item__arg : pattern -> pattern
val desc_of_pattern : pattern -> Prims.string
val string_of_pattern : pattern -> Prims.string
type match_exception =
  1. | NameMismatch of qn * qn
  2. | SimpleMismatch of pattern * FStar_Reflection_Types.term
  3. | NonLinearMismatch of varname * FStar_Reflection_Types.term * FStar_Reflection_Types.term
  4. | UnsupportedTermInPattern of FStar_Reflection_Types.term
  5. | IncorrectTypeInAbsPatBinder of FStar_Reflection_Types.typ
val uu___is_NameMismatch : match_exception -> Prims.bool
val __proj__NameMismatch__item___0 : match_exception -> qn * qn
val uu___is_SimpleMismatch : match_exception -> Prims.bool
val __proj__SimpleMismatch__item___0 : match_exception -> pattern * FStar_Reflection_Types.term
val uu___is_NonLinearMismatch : match_exception -> Prims.bool
val __proj__NonLinearMismatch__item___0 : match_exception -> varname * FStar_Reflection_Types.term * FStar_Reflection_Types.term
val uu___is_UnsupportedTermInPattern : match_exception -> Prims.bool
val __proj__UnsupportedTermInPattern__item___0 : match_exception -> FStar_Reflection_Types.term
val uu___is_IncorrectTypeInAbsPatBinder : match_exception -> Prims.bool
val __proj__IncorrectTypeInAbsPatBinder__item___0 : match_exception -> FStar_Reflection_Types.typ
type !'a match_res =
  1. | Success of 'a
  2. | Failure of match_exception
val uu___is_Success : 'a match_res -> Prims.bool
val __proj__Success__item___0 : 'a match_res -> 'a
val uu___is_Failure : 'a match_res -> Prims.bool
val __proj__Failure__item___0 : 'a match_res -> match_exception
val return : 'a -> 'a match_res
val raise : match_exception -> 'a match_res
val lift_exn_tac : ('a -> 'b match_res) -> 'a -> FStar_Tactics_Types.proofstate -> 'b FStar_Tactics_Result.__result
val lift_exn_tactic : ('a -> 'b match_res) -> 'a -> FStar_Tactics_Types.proofstate -> 'b FStar_Tactics_Result.__result
type matching_problem = {
  1. mp_vars : varname Prims.list;
  2. mp_hyps : (varname * pattern) Prims.list;
  3. mp_goal : pattern FStar_Pervasives_Native.option;
}
val __proj__Mkmatching_problem__item__mp_vars : matching_problem -> varname Prims.list
val __proj__Mkmatching_problem__item__mp_hyps : matching_problem -> (varname * pattern) Prims.list
val __proj__Mkmatching_problem__item__mp_goal : matching_problem -> pattern FStar_Pervasives_Native.option
val string_of_matching_problem : matching_problem -> Prims.string
type matching_solution = {
  1. ms_vars : (varname * FStar_Reflection_Types.term) Prims.list;
  2. ms_hyps : (varname * hypothesis) Prims.list;
}
val __proj__Mkmatching_solution__item__ms_vars : matching_solution -> (varname * FStar_Reflection_Types.term) Prims.list
val __proj__Mkmatching_solution__item__ms_hyps : matching_solution -> (varname * hypothesis) Prims.list
val ms_locate_unit : 'uuuuu -> 'uuuuu1 -> FStar_Tactics_Types.proofstate -> Prims.unit FStar_Tactics_Result.__result
val __ : Prims.unit -> 't
val any_qn : Prims.string
type 'a pm_goal = Prims.unit
val hyp_qn : Prims.string
val goal_qn : Prims.string
type abspat_binder_kind =
  1. | ABKVar of FStar_Reflection_Types.typ
  2. | ABKHyp
  3. | ABKGoal
val uu___is_ABKVar : abspat_binder_kind -> Prims.bool
val __proj__ABKVar__item___0 : abspat_binder_kind -> FStar_Reflection_Types.typ
val uu___is_ABKHyp : abspat_binder_kind -> Prims.bool
val uu___is_ABKGoal : abspat_binder_kind -> Prims.bool
val string_of_abspat_binder_kind : abspat_binder_kind -> Prims.string
type abspat_argspec = {
  1. asa_name : absvar;
  2. asa_kind : abspat_binder_kind;
}
val __proj__Mkabspat_argspec__item__asa_name : abspat_argspec -> absvar
val __proj__Mkabspat_argspec__item__asa_kind : abspat_argspec -> abspat_binder_kind
val locate_fn_of_binder_kind : abspat_binder_kind -> FStar_Reflection_Types.term