package fstar

You can search for identifiers within the package.

in-package search v0.2.0

package fstar

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type heap2 = FStar_Monotonic_Heap.heap FStar_Relational_Relational.double

type st2_Pre = Prims.unit

type ('a, 'pre) st2_Post' = Prims.unit

type 'a st2_Post = Prims.unit

type 'a st2_WP = Prims.unit

type ('a, 'b, !'wp0, 'wp1, 'p, 'h2) comp = 'wp0

val compose2 : 
  ('a0 -> 'b0) ->
  ('a1 -> 'b1) ->
  ('a0, 'a1) FStar_Relational_Relational.rel ->
  ('b0, 'b1) FStar_Relational_Relational.rel

val compose2_self : 
  ('a -> 'b) ->
  'a FStar_Relational_Relational.double ->
  'b FStar_Relational_Relational.double

val cross : 
  (Prims.unit FStar_Relational_Relational.double ->
    ('a, 'b) FStar_Relational_Relational.rel) ->
  (Prims.unit FStar_Relational_Relational.double ->
    ('c, 'd) FStar_Relational_Relational.rel) ->
  ('a, 'd) FStar_Relational_Relational.rel

type ('a0, 'a1, 'b0, 'b1, 'al, 'wp, 'p, 'hl) decomp_l = Prims.unit

type ('a0, 'a1, 'b0, 'b1, 'ar, 'wp, 'p, 'hr) decomp_r = Prims.unit

val project_l : 
  (('a0, 'a1) FStar_Relational_Relational.rel ->
    ('b0, 'b1) FStar_Relational_Relational.rel) ->
  'a0 ->
  'b0

val project_r : 
  (('a0, 'a1) FStar_Relational_Relational.rel ->
    ('b0, 'b1) FStar_Relational_Relational.rel) ->
  'a1 ->
  'b1