What4.Expr.AppTheory

Documentation

data AppTheory

The theory that a symbol belongs to.

Constructors

BoolTheory

LinearArithTheory

NonlinearArithTheory

ComputableArithTheory

BitvectorTheory

QuantifierTheory

StringTheory

FloatingPointTheory

ArrayTheory

StructTheory

Theory attributed to structs (equivalent to records in CVC4/Z3, tuples in Yices)

FnTheory

Theory attributed application functions.

Instances

Eq AppTheory

Defined in What4.Expr.AppTheory

Methods

(==) :: AppTheory -> AppTheory -> Bool

(/=) :: AppTheory -> AppTheory -> Bool

Ord AppTheory

Defined in What4.Expr.AppTheory

Methods

compare :: AppTheory -> AppTheory -> Ordering

(<) :: AppTheory -> AppTheory -> Bool

(<=) :: AppTheory -> AppTheory -> Bool

(>) :: AppTheory -> AppTheory -> Bool

(>=) :: AppTheory -> AppTheory -> Bool

max :: AppTheory -> AppTheory -> AppTheory

min :: AppTheory -> AppTheory -> AppTheory

quantTheory :: NonceApp t (Expr t) tp -> AppTheory

appTheory :: App (Expr t) tp -> AppTheory

typeTheory :: BaseTypeRepr tp -> AppTheory