fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type (!'a, !'r, !'x) acc =
  1. | AccIntro of 'a -> 'r -> ('a, 'r, Prims.unit) acc
val uu___is_AccIntro : 'a -> ('a, 'r, Prims.unit) acc -> Prims.bool
val __proj__AccIntro__item___0 : 'a -> ('a, 'r, Prims.unit) acc -> 'a -> 'r -> ('a, 'r, Prims.unit) acc
type (!'a, !'r) well_founded = 'a -> ('a, 'r, Prims.unit) acc
val acc_inv : 'aa -> ('aa, 'r, Prims.unit) acc -> 'aa -> 'r -> ('aa, 'r, Prims.unit) acc
val fix_F : ('aa -> ('aa -> 'r -> 'p) -> 'p) -> 'aa -> ('aa, 'r, Prims.unit) acc -> 'p
val fix : ('aa, 'r) well_founded -> Prims.unit -> ('aa -> ('aa -> 'r -> Obj.t) -> Obj.t) -> 'aa -> Obj.t
type ('a, 'rel) is_well_founded = Prims.unit
type 'a well_founded_relation = Prims.unit
type ('a, !'rel, 'f, 'uuuuu, 'uuuuu1) as_well_founded = 'rel
val subrelation_wf : ('a -> 'a -> 'subur -> 'r) -> ('a, 'r) well_founded -> ('a, 'subur) well_founded
type ('a, 'r, !'subur, 'subuw, 'ruwf, 'uuuuu, 'uuuuu1) subrelation_as_wf = 'subur
type ('a, 'b, !'rub, 'f, 'x, 'y) inverse_image = 'rub
val inverse_image_wf : ('a -> 'b) -> ('b, 'rub) well_founded -> ('a, 'rub) well_founded