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 'n bv_t = Prims.unit FStar_BitVector.bv_t

val bv_uext : 
  Prims.pos ->
  Prims.pos ->
  Prims.unit bv_t ->
  Prims.bool FStar_Seq_Base.seq

val int2bv : Prims.pos -> Prims.unit FStar_UInt.uint_t -> Prims.unit bv_t

val bv2int : Prims.pos -> Prims.unit bv_t -> Prims.unit FStar_UInt.uint_t

val int2bv_nat : Prims.pos -> Prims.nat -> Prims.unit bv_t

val list2bv : Prims.pos -> Prims.bool Prims.list -> Prims.unit bv_t

val bv2list : Prims.pos -> Prims.unit bv_t -> Prims.bool Prims.list

val bvand : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.unit bv_t

val bvxor : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.unit bv_t

val bvor : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.unit bv_t

val bvnot : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t

val bvshl' : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.unit bv_t

val bvshl : Prims.pos -> Prims.unit bv_t -> Prims.nat -> Prims.unit bv_t

val bvshr' : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.unit bv_t

val bvshr : Prims.pos -> Prims.unit bv_t -> Prims.nat -> Prims.unit bv_t

val bv_zero : Prims.pos -> Prims.unit bv_t

val bvult : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.bool

val bvadd : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.unit bv_t

val bvsub : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.unit bv_t

val bvdiv : 
  Prims.pos ->
  Prims.unit bv_t ->
  Prims.unit FStar_UInt.uint_t ->
  Prims.unit bv_t

val bvdiv_unsafe : 
  Prims.pos ->
  Prims.unit bv_t ->
  Prims.unit bv_t ->
  Prims.unit bv_t

val bvmod : 
  Prims.pos ->
  Prims.unit bv_t ->
  Prims.unit FStar_UInt.uint_t ->
  Prims.unit bv_t

val bvmod_unsafe : 
  Prims.pos ->
  Prims.unit bv_t ->
  Prims.unit bv_t ->
  Prims.unit bv_t

val bvmul : 
  Prims.pos ->
  Prims.unit bv_t ->
  Prims.unit FStar_UInt.uint_t ->
  Prims.unit bv_t

val bvmul' : Prims.pos -> Prims.unit bv_t -> Prims.unit bv_t -> Prims.unit bv_t