fstar 2022.01.15 · OCaml Package

To focus the search input from anywhere on the page, press the 'S' key.

in-package search v0.1.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type (!'t, !'dummyV0, !'dummyV1, !'dummyV2) calc_proof =

| CalcRefl of 't
| CalcStep of Prims.unit Prims.list * Prims.unit * 't * 't * 't * ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof * Prims.unit

val uu___is_CalcRefl : 
  Prims.unit Prims.list ->
  't ->
  't ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof ->
  Prims.bool

val __proj__CalcRefl__item__x : 
  Prims.unit Prims.list ->
  't ->
  't ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof ->
  't

val uu___is_CalcStep : 
  Prims.unit Prims.list ->
  't ->
  't ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof ->
  Prims.bool

val __proj__CalcStep__item__rs : 
  Prims.unit Prims.list ->
  't ->
  't ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof ->
  Prims.unit Prims.list

val __proj__CalcStep__item__x : 
  Prims.unit Prims.list ->
  't ->
  't ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof ->
  't

val __proj__CalcStep__item__y : 
  Prims.unit Prims.list ->
  't ->
  't ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof ->
  't

val __proj__CalcStep__item__z : 
  Prims.unit Prims.list ->
  't ->
  't ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof ->
  't

val __proj__CalcStep__item___5 : 
  Prims.unit Prims.list ->
  't ->
  't ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof

type (!'t, !'x, !'y) calc_pack = {

rels : Prims.unit Prims.list;
proof : ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof;

}

val __proj__Mkcalc_pack__item__rels : 
  't ->
  't ->
  ('t, Prims.unit, Prims.unit) calc_pack ->
  Prims.unit Prims.list

val __proj__Mkcalc_pack__item__proof : 
  't ->
  't ->
  ('t, Prims.unit, Prims.unit) calc_pack ->
  ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof

val pk_rels : 
  't ->
  't ->
  ('t, Prims.unit, Prims.unit) calc_pack ->
  Prims.unit Prims.list

type ('t, 'rs, 'x, 'y) calc_chain_related = Obj.t

type ('t, 'rs, 'p) calc_chain_compatible = Prims.unit

val _calc_init : 't -> ('t, Prims.unit, Prims.unit, Prims.unit) calc_proof

val calc_init : 't -> ('t, Prims.unit, Prims.unit) calc_pack