package fstar

You can search for identifiers within the package.

in-package search v0.2.0

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type sw = FStar_Integers.signed_width

type ('sl, 'l, 's) secret_int =
  (Prims.unit, Prims.unit, Obj.t) FStar_IFC.protected

val promote : 
  Prims.unit ->
  Prims.unit ->
  sw ->
  (Prims.unit, Prims.unit, Prims.unit) secret_int ->
  Prims.unit ->
  (Prims.unit, Prims.unit, Prims.unit) secret_int

type qual =

| Secret of Prims.unit * Prims.unit * sw
| Public of FStar_Integers.signed_width

val uu___is_Secret : qual -> Prims.bool

val __proj__Secret__item__sw : qual -> sw

val uu___is_Public : qual -> Prims.bool

val __proj__Public__item__sw : qual -> FStar_Integers.signed_width

val sw_qual : qual -> FStar_Integers.signed_width

type 'q t = Obj.t

val as_secret : 
  qual ->
  Obj.t ->
  (Prims.unit, Prims.unit, Prims.unit) secret_int

val as_public : qual -> Obj.t -> Obj.t