package fstar

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type 'a symrel = Prims.unit

type !'a pcm' = {

}

val __proj__Mkpcm'__item__op : 'a pcm' -> 'a -> 'a -> 'a

val __proj__Mkpcm'__item__one : 'a pcm' -> 'a

type ('a, 'p) lem_commutative = Prims.unit

type ('a, 'p) lem_assoc_l = Prims.unit

type ('a, 'p) lem_assoc_r = Prims.unit

type ('a, 'p) lem_is_unit = Prims.unit

type !'a pcm = {

}

val __proj__Mkpcm__item__p : 'a pcm -> 'a pcm'

type ('a, 'p, 'x, 'y) composable = Obj.t

val op : 'a pcm -> 'a -> 'a -> 'a

type ('a, 'pcm1, 'x, 'y) compatible = Prims.unit

type ('a, 'p, 'x, 'y) joinable = Prims.unit

type ('a, 'p, 'x, 'v, 'y) frame_compatible = Prims.unit

type (!'a, 'p, 'x, 'y) frame_preserving_upd = 'a -> 'a

type ('a, 'pcm1, 'x, 'y) frame_preserving = Prims.unit

val frame_preserving_val_to_fp_upd : 'a pcm -> Prims.unit -> 'a -> 'a -> 'a

type ('a, 'p, 'x) exclusive = Prims.unit

val no_op_is_frame_preserving : 'a pcm -> 'a -> 'a -> 'a

val compose_frame_preserving_updates : 
  'a pcm ->
  'a ->
  'a ->
  'a ->
  ('a -> 'a) ->
  ('a -> 'a) ->
  'a ->
  'a

val frame_preserving_subframe : 
  'a pcm ->
  'a ->
  'a ->
  'a ->
  ('a -> 'a) ->
  'a ->
  'a