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 'k less_than = Prims.int

type 'k greater_than = Prims.int

type 'x not_less_than = Prims.unit greater_than

type 'x not_greater_than = Prims.unit less_than

val coerce_to_less_than : 
  Prims.int ->
  Prims.unit not_greater_than ->
  Prims.unit less_than

val coerce_to_not_less_than : 
  Prims.int ->
  Prims.unit greater_than ->
  Prims.unit not_less_than

val interval_condition : Prims.int -> Prims.int -> Prims.int -> Prims.bool

type ('x, 'y) interval_type = Prims.unit

type ('x, 'y) interval = Prims.int

type ('x, 'y) efrom_eto = (Prims.unit, Prims.unit) interval

type ('x, 'y) efrom_ito = (Prims.unit, Prims.unit) interval

type ('x, 'y) ifrom_eto = (Prims.unit, Prims.unit) interval

type ('x, 'y) ifrom_ito = (Prims.unit, Prims.unit) interval

type 'k under = (Prims.unit, Prims.unit) interval

val interval_size : Prims.int -> Prims.int -> Prims.unit -> Prims.nat

type ('x, 'y, 'interval1) counter_for = Prims.unit under

val closed_interval_size : Prims.int -> Prims.int -> Prims.nat

val indices_seq : Prims.nat -> Prims.unit under FStar_Seq_Base.seq