Copyright	(c) Galois Inc 2016-2020
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

What4.Expr.AppTheory

Description

Synopsis

Documentation

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 details

Eq AppTheory Source #
Instance details Defined in What4.Expr.AppTheory Methods (==) :: AppTheory -> AppTheory -> Bool # (/=) :: AppTheory -> AppTheory -> Bool #
Ord AppTheory Source #
Instance details 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 #