Copyright | (c) Galois Inc 2014-2020 |
---|---|
License | BSD3 |
Maintainer | Joe Hendrix <[email protected]> |
Stability | provisional |
Safe Haskell | None |
Language | Haskell2010 |
What4.BaseTypes
Description
This module exports the types used in solver expressions.
These types are largely used as indexes to various GADTs and type families as a way to let the GHC typechecker help us keep expressions used by solvers apart.
In addition, we provide a value-level reification of the type
indices that can be examined by pattern matching, called BaseTypeRepr
.
Synopsis
- data BaseType
- type BaseBoolType = 'BaseBoolType
- type BaseIntegerType = 'BaseIntegerType
- type BaseRealType = 'BaseRealType
- type BaseStringType = 'BaseStringType
- type BaseBVType = 'BaseBVType
- type BaseFloatType = 'BaseFloatType