fstar 2025.02.17 (latest) · OCaml Package

type 'a binrel = Prims.unit

type 'a predicate = Prims.unit

type ('a, 'rel) reflexive = Prims.unit

type ('a, 'rel) transitive = Prims.unit

type ('a, 'rel) preorder_rel = Prims.unit

type 'a preorder = Prims.unit

type ('a, 'p, 'rel) stable = Prims.unit

type (!'a, !'r, !'dummyV0, !'dummyV1) _closure =

| Refl of 'a
| Step of 'a * 'a * Prims.unit
| Closure of 'a * 'a * 'a * ('a, 'r, Prims.unit, Prims.unit) _closure * ('a, 'r, Prims.unit, Prims.unit) _closure

val uu___is_Refl : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  Prims.bool

val __proj__Refl__item__x : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  'a

val uu___is_Step : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  Prims.bool

val __proj__Step__item__x : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  'a

val __proj__Step__item__y : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  'a

val uu___is_Closure : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  Prims.bool

val __proj__Closure__item__x : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  'a

val __proj__Closure__item__y : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  'a

val __proj__Closure__item__z : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  'a

val __proj__Closure__item___3 : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  ('a, 'r, Prims.unit, Prims.unit) _closure

val __proj__Closure__item___4 : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  ('a, 'r, Prims.unit, Prims.unit) _closure

type ('a, 'r, 'x, 'y) _closure0 = Prims.unit

type ('a, 'r, 'uuuuu, 'uuuuu1) closure = Prims.unit

val closure_one_aux : 
  'a ->
  'a ->
  ('a, 'r, Prims.unit, Prims.unit) _closure ->
  (Prims.unit,
    ('a, Prims.unit, ('a, 'r, Prims.unit, Prims.unit) _closure)
      FStar_Pervasives.dtuple3)
    FStar_Pervasives.either

package fstar