Copyright | (c) Christian Maeder DFKI GmbH 2008 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Common.Consistency
Description
Data types for conservativity
- data Conservativity
- showConsistencyStatus :: Conservativity -> String
- data ConservativityChecker sign sentence morphism = ConservativityChecker {
- checkerId :: String
- checkerUsable :: IO (Maybe String)
- checkConservativity :: (sign, [Named sentence]) -> morphism -> [Named sentence] -> IO (Result (Conservativity, [sentence]))
Documentation
data Conservativity Source #
Conservativity annotations. For compactness, only the greatest applicable value is used in a DG. PCons stands for prooftheoretic conservativity as required for extending imports (no confusion) in Maude
Instances
Eq Conservativity Source # | |
Data Conservativity Source # | |
Ord Conservativity Source # | |
Read Conservativity Source # | |
Show Conservativity Source # | |
Pretty Conservativity Source # | |
showConsistencyStatus :: Conservativity -> String Source #
data ConservativityChecker sign sentence morphism Source #
All target sentences must be implied by the source translated along the morphism. They are axioms only and not identical to any translated sentence of the source.
Constructors
ConservativityChecker | |
Fields
|