Module Theory.Bitv

Sorts of bitvectors

type 'a t
val define : int -> 'a t Value.sort

define size defines a sort of bitvectors of the given size.

val refine : unit Value.sort -> 'a t Value.sort option

refine s if s is a bitvector sort, then restores its type.

val size : 'a t Value.sort -> int

size s the size argument of s.