fstar 2025.02.17 · OCaml Package

type (!'a, !'b) rel =

| R of 'a * 'b

val uu___is_R : ('a, 'b) rel -> Prims.bool

val __proj__R__item__l : ('a, 'b) rel -> 'a

val __proj__R__item__r : ('a, 'b) rel -> 'b

type !'t double = ('t, 't) rel

type !'t eq = 't double

val twice : 'uuuuu -> ('uuuuu, 'uuuuu) rel

val tu : (Prims.unit, Prims.unit) rel

val rel_map1T : ('a -> 'b) -> 'a double -> 'b double

val rel_map2Teq : ('a -> 'b -> 'c) -> 'a double -> 'b double -> 'c double

val rel_map2T : ('a -> 'b -> 'c) -> 'a double -> 'b double -> 'c double

val rel_map3T : 
  ('a -> 'b -> 'c -> 'd) ->
  'a double ->
  'b double ->
  'c double ->
  'd double

val op_Hat_Plus : Prims.int double -> Prims.int double -> Prims.int double

val op_Hat_Minus : Prims.int double -> Prims.int double -> Prims.int double

val op_Hat_Star : Prims.int double -> Prims.int double -> Prims.int double

val op_Hat_Slash : Prims.int double -> Prims.nonzero double -> Prims.int double

val tl_rel : 'a Prims.list double -> 'a Prims.list double

val cons_rel : 
  ('uuuuu, 'uuuuu1) rel ->
  ('uuuuu Prims.list, 'uuuuu1 Prims.list) rel ->
  ('uuuuu Prims.list, 'uuuuu1 Prims.list) rel

val pair_rel : 
  ('uuuuu, 'uuuuu1) rel ->
  ('uuuuu2, 'uuuuu3) rel ->
  ('uuuuu * 'uuuuu2, 'uuuuu1 * 'uuuuu3) rel

val triple_rel : 
  ('uuuuu, 'uuuuu1) rel ->
  ('uuuuu2, 'uuuuu3) rel ->
  ('uuuuu4, 'uuuuu5) rel ->
  ('uuuuu * 'uuuuu2 * 'uuuuu4, 'uuuuu1 * 'uuuuu3 * 'uuuuu5) rel

val fst_rel : Prims.unit -> ('uuuuu * 'uuuuu1) double -> 'uuuuu double

val snd_rel : Prims.unit -> ('uuuuu * 'uuuuu1) double -> 'uuuuu1 double

val and_rel : Prims.bool double -> Prims.bool double -> Prims.bool double

val or_rel : Prims.bool double -> Prims.bool double -> Prims.bool double

val eq_rel : Prims.bool double -> Prims.bool double -> Prims.bool double

val and_irel : (Prims.bool, Prims.bool) rel -> Prims.bool

val or_irel : (Prims.bool, Prims.bool) rel -> Prims.bool

val eq_irel : ('t, 't) rel -> Prims.bool

package fstar