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

Orphan instances

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 #
Methods toShATermAux :: ATermTable -> ProverKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ProverKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ProverKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProverKind])
ShATermConvertible GoalStatus Source #
Methods toShATermAux :: ATermTable -> GoalStatus -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GoalStatus] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GoalStatus) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GoalStatus])
ShATermConvertible Reason Source #
Methods toShATermAux :: ATermTable -> Reason -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Reason] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Reason) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Reason])
ShATermConvertible TacticScript Source #
Methods toShATermAux :: ATermTable -> TacticScript -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TacticScript] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TacticScript) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TacticScript])
ShATermConvertible proof_tree => ShATermConvertible (CCStatus proof_tree) Source #
Methods toShATermAux :: ATermTable -> CCStatus proof_tree -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [CCStatus proof_tree] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, CCStatus proof_tree) fromShATermList' :: Int -> ATermTable -> (ATermTable, [CCStatus proof_tree])
ShATermConvertible proof_tree => ShATermConvertible (ProofStatus proof_tree) Source #
Methods toShATermAux :: ATermTable -> ProofStatus proof_tree -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ProofStatus proof_tree] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofStatus proof_tree) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofStatus proof_tree])
ShATermConvertible a => ShATermConvertible (ThmStatus a) Source #
Methods toShATermAux :: ATermTable -> ThmStatus a -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ThmStatus a] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ThmStatus a) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ThmStatus a])
(ShATermConvertible sentence, ShATermConvertible morphism) => ShATermConvertible (FreeDefMorphism sentence morphism) Source #
Methods toShATermAux :: ATermTable -> FreeDefMorphism sentence morphism -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FreeDefMorphism sentence morphism] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FreeDefMorphism sentence morphism) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FreeDefMorphism sentence morphism])
(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible proof_tree) => ShATermConvertible (Theory sign sen proof_tree) Source #
Methods toShATermAux :: ATermTable -> Theory sign sen proof_tree -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Theory sign sen proof_tree] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Theory sign sen proof_tree) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Theory sign sen proof_tree])
(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible mor, ShATermConvertible proof_tree) => ShATermConvertible (TheoryMorphism sign sen mor proof_tree) Source #
Methods toShATermAux :: ATermTable -> TheoryMorphism sign sen mor proof_tree -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TheoryMorphism sign sen mor proof_tree] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TheoryMorphism sign sen mor proof_tree) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TheoryMorphism sign sen mor proof_tree])