fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
val op_At : 'uuuuu Prims.list -> 'uuuuu Prims.list -> 'uuuuu Prims.list
type true_p = Prims.unit
type ('a, 'hp) selector' = Prims.unit
type ('a, 'hp, 'sel) sel_depends_only_on = Prims.unit
type ('a, 'hp, 'sel) sel_depends_only_on_core = Prims.unit
type ('a, 'hp) selector = Prims.unit
type vprop' = {
  1. hp : Prims.unit;
  2. t : Prims.unit;
  3. sel : Prims.unit;
}
val to_vprop' : Prims.unit -> vprop'
val normal : 'a -> 'a
type 'p t_of = Obj.t
type pre_t = Prims.unit
type 'a post_t = Prims.unit
type ('p, 'q) can_be_split = Prims.unit
type ('a, 'p, 'q) can_be_split_forall = Prims.unit
type ('p, 't1, 't2) can_be_split_dep = Prims.unit
type ('a, 'p, 't1, 't2) can_be_split_forall_dep = Prims.unit
type ('a, 't1, 't2) equiv_forall = Prims.unit
type ('a, 'b, 't1, 't2) can_be_split_post = Prims.unit
type ('p, 'q) equiv = Prims.unit
type 'pre rmem' = Prims.unit
type ('frame, 'h) valid_rmem = Prims.unit
type 'pre rmem = Prims.unit
type 'pre req_t = Prims.unit
type ('pre, 'a, 'post) ens_t = Prims.unit
val emp' : vprop'
type ('framed, 'frame) maybe_emp = Obj.t
type ('a, 'framed, 'frame) maybe_emp_dep = Obj.t
type ('frame, 'h0, 'h1) frame_equalities' = Obj.t
type ('frame, 'h0, 'h1) frame_equalities = Obj.t
type ('v, !'p) vrefine_am = 'p
type ('v, 'p) vrefine_t = Obj.t
val vrefine' : Prims.unit -> Prims.unit -> vprop'
type ('v, 'p, 'x) vdep_payload = Obj.t
type ('v, 'p) vdep_t = (Obj.t, Obj.t) Prims.dtuple2
val vdep' : Prims.unit -> Prims.unit -> vprop'
val vrewrite' : Prims.unit -> Prims.unit -> Prims.unit -> vprop'
exception Appears
val uu___is_Appears : Prims.exn -> Prims.bool
type atom = Prims.int
val atoms_to_string : atom Prims.list -> Prims.string
type exp =
  1. | Unit
  2. | Mult of exp * exp
  3. | Atom of atom
val uu___is_Unit : exp -> Prims.bool
val uu___is_Mult : exp -> Prims.bool
val __proj__Mult__item___0 : exp -> exp
val __proj__Mult__item___1 : exp -> exp
val uu___is_Atom : exp -> Prims.bool
val __proj__Atom__item___0 : exp -> atom
type !'a amap = (atom * 'a) Prims.list * 'a
val const : 'a -> 'a amap
val select : atom -> 'a amap -> 'a
val update : atom -> 'a -> 'a amap -> 'a amap
val trivial_cancel : atom -> atom Prims.list -> Prims.bool * atom Prims.list
exception Failed
val uu___is_Failed : Prims.exn -> Prims.bool
exception Success
val uu___is_Success : Prims.exn -> Prims.bool
val mdenote_gen : 'a -> ('a -> 'a -> 'a) -> 'a amap -> exp -> 'a
val xsdenote_gen : 'a -> ('a -> 'a -> 'a) -> 'a amap -> atom Prims.list -> 'a
val flatten : exp -> atom Prims.list
type permute = atom Prims.list -> atom Prims.list
val sort : permute
val quote_exp : exp -> FStar_Reflection_Types.term
val normal_tac_steps : FStar_Pervasives.norm_step Prims.list
val normal_tac : 'a -> 'a
val uu___is_Result : Prims.exn -> Prims.bool
val __proj__Result__item__uu___ : Prims.exn -> atom Prims.list * atom Prims.list * Prims.bool * FStar_Reflection_Types.term Prims.list
val solve_can_be_split_post : FStar_Reflection_Data.argv Prims.list -> FStar_Tactics_Types.proofstate -> Prims.bool FStar_Tactics_Result.__result
type observability =
  1. | Observable
  2. | Unobservable
val uu___is_Observable : observability -> Prims.bool
val uu___is_Unobservable : observability -> Prims.bool
val obs_at_most_one : observability -> observability -> Prims.bool
type 'p inv = Prims.unit