fstar 2025.02.17 · OCaml Package

type (!'a, !'r, !'x) acc_classical =

val uu___is_AccClassicalIntro : 
  'a ->
  ('a, 'r, Prims.unit) acc_classical ->
  Prims.bool

val __proj__AccClassicalIntro__item__access_smaller : 
  'a ->
  ('a, 'r, Prims.unit) acc_classical ->
  'a ->
  ('a, 'r, Prims.unit) acc_classical

type !'a wfr_t = {

}

val __proj__Mkwfr_t__item__decreaser : 
  'a wfr_t ->
  'a ->
  ('a, Prims.unit, Prims.unit) acc_classical

type ('a, 'x1, 'x2) default_relation =
  ('a, 'a, Prims.unit, Prims.unit) Prims.precedes

val default_decreaser : 'a -> ('a, Prims.unit, Prims.unit) acc_classical

val default_wfr : Prims.unit -> 'a wfr_t

type ('a, 'x1, 'x2) empty_relation = Prims.unit

val empty_decreaser : 'a -> ('a, Prims.unit, Prims.unit) acc_classical

val empty_wfr : Prims.unit -> 'a wfr_t

type ('a, 'r, 'x1, 'x2) acc_relation = Prims.unit

val acc_decreaser : 
  Prims.unit ->
  'a ->
  ('a, Prims.unit, Prims.unit) acc_classical

val acc_to_wfr : Prims.unit -> 'a wfr_t

val subrelation_decreaser : 
  'a wfr_t ->
  'a ->
  ('a, 'r, Prims.unit) acc_classical

val subrelation_to_wfr : 'a wfr_t -> 'a wfr_t

val inverse_image_decreaser : 
  ('a -> 'b) ->
  'b wfr_t ->
  'a ->
  ('a, 'r, Prims.unit) acc_classical

val inverse_image_to_wfr : ('a -> 'b) -> 'b wfr_t -> 'a wfr_t

type ('a, 'b, 'wfrua, 'wfrub, 'xy1, 'xy2) lex_nondep_relation = Obj.t

val lex_nondep_decreaser : 
  'a wfr_t ->
  'b wfr_t ->
  ('a * 'b) ->
  ('a * 'b, Obj.t, Prims.unit) acc_classical

val lex_nondep_wfr : 'a wfr_t -> 'b wfr_t -> ('a * 'b) wfr_t

type ('a, 'b, 'wfrua, 'autouwfrub, 'xy1, 'xy2) lex_dep_relation = Obj.t

val lex_dep_decreaser : 
  'a wfr_t ->
  ('a -> 'b wfr_t) ->
  ('a, 'b) Prims.dtuple2 ->
  (('a, 'b) Prims.dtuple2, Obj.t, Prims.unit) acc_classical

val lex_dep_wfr : 'a wfr_t -> ('a -> 'b wfr_t) -> ('a, 'b) Prims.dtuple2 wfr_t

type ('x1, 'x2) bool_relation = Prims.unit

val bool_wfr : Prims.bool wfr_t

type ('a, 'wfr, 'opt1, 'opt2) option_relation = Prims.unit

val option_wfr : 'a wfr_t -> 'a FStar_Pervasives_Native.option wfr_t

package fstar