grisette-0.13.0.1: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2024
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Internal.Unified.Theories

Description

 
Synopsis

Documentation

data TheoryToUnify Source #

This data type is used to represent the theories that is unified.

The UFun constructor is used to represent a specific uninterpreted function type. The type is uncurried.

Constructors

UBool 
UIntN 
UWordN 
UInteger 
UAlgReal 
UFP 
UFun [TheoryToUnify] 

Instances

Instances details
Show TheoryToUnify Source # 
Instance details

Defined in Grisette.Internal.Unified.Theories

Methods

showsPrec :: Int -> TheoryToUnify -> ShowS #

show :: TheoryToUnify -> String #

showList :: [TheoryToUnify] -> ShowS #

Eq TheoryToUnify Source # 
Instance details

Defined in Grisette.Internal.Unified.Theories

Methods

(==) :: TheoryToUnify -> TheoryToUnify -> Bool #

(/=) :: TheoryToUnify -> TheoryToUnify -> Bool #

isUFun :: TheoryToUnify -> Bool Source #

Check if the theory is a uninterpreted function.