To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
package fstar
-
fstarlib
-
fstartaclib
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type st2_Pre = Prims.unittype ('a, 'pre) st2_Post' = Prims.unittype 'a st2_Post = Prims.unittype 'a st2_WP = Prims.unitval compose2 :
('a0 -> 'b0) ->
('a1 -> 'b1) ->
('a0, 'a1) FStar_Relational_Relational.rel ->
('b0, 'b1) FStar_Relational_Relational.relval compose2_self :
('a -> 'b) ->
'a FStar_Relational_Relational.double ->
'b FStar_Relational_Relational.doubleval 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.reltype ('a0, 'a1, 'b0, 'b1, 'al, 'wp, 'p, 'hl) decomp_l = Prims.unittype ('a0, 'a1, 'b0, 'b1, 'ar, 'wp, 'p, 'hr) decomp_r = Prims.unitval project_l :
(('a0, 'a1) FStar_Relational_Relational.rel ->
('b0, 'b1) FStar_Relational_Relational.rel) ->
'a0 ->
'b0val project_r :
(('a0, 'a1) FStar_Relational_Relational.rel ->
('b0, 'b1) FStar_Relational_Relational.rel) ->
'a1 ->
'b1