Copyright | (c) DFKI GmbH 2012 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | non-portable(derive Typeable instances) |
Safe Haskell | None |
ATC.Prover
Contents
Description
Automatic derivation of instances via DrIFT-rule ShATermConvertible
for the type(s):
ThmStatus
Theory
TacticScript
Reason
GoalStatus
ProofStatus
ProverKind
FreeDefMorphism
TheoryMorphism
CCStatus
Orphan instances
ShATermConvertible ProverKind Source # | |
ShATermConvertible GoalStatus Source # | |
ShATermConvertible Reason Source # | |
ShATermConvertible TacticScript Source # | |
ShATermConvertible proof_tree => ShATermConvertible (CCStatus proof_tree) Source # | |
ShATermConvertible proof_tree => ShATermConvertible (ProofStatus proof_tree) Source # | |
ShATermConvertible a => ShATermConvertible (ThmStatus a) Source # | |
(ShATermConvertible sentence, ShATermConvertible morphism) => ShATermConvertible (FreeDefMorphism sentence morphism) Source # | |
(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible proof_tree) => ShATermConvertible (Theory sign sen proof_tree) Source # | |
(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible mor, ShATermConvertible proof_tree) => ShATermConvertible (TheoryMorphism sign sen mor proof_tree) Source # | |