kdrag.theories

Library of axioms, theorems, and theory specific tactics

Modules

bitvec	Theorems about bitvectors.
bool
fixed	Theory of fixed point arithmetic
float	Theory of built in floating point and connection to the reals
fun
int	Builtin theory of integers
list	Algebraic datatype of lists.
nat	Algebraic datatype for the Peano natural numbers
option	Algebraic data type for optional values
real	Definitions about the reals.
regex	Theory of regular expressions
seq	Built in smtlib theory of finite sequences.
set	First class sets ArraySort(T, Bool)