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

HolLight.ATC_HolLight

Contents

Orphan instances

Description

Automatic derivation of instances via DrIFT-rule ShATermConvertible, Json for the type(s): Sentence Sign HolLightSL HolType HolProof HolParseType HolTermInfo Term

Orphan instances

Generic HolLightSL Source #
Instance details Associated Types type Rep HolLightSL :: Type -> Type Methods from :: HolLightSL -> Rep HolLightSL x to :: Rep HolLightSL x -> HolLightSL
Generic Term Source #
Instance details Associated Types type Rep Term :: Type -> Type Methods from :: Term -> Rep Term x to :: Rep Term x -> Term
Generic HolTermInfo Source #
Instance details Associated Types type Rep HolTermInfo :: Type -> Type Methods from :: HolTermInfo -> Rep HolTermInfo x to :: Rep HolTermInfo x -> HolTermInfo
Generic HolParseType Source #
Instance details Associated Types type Rep HolParseType :: Type -> Type Methods from :: HolParseType -> Rep HolParseType x to :: Rep HolParseType x -> HolParseType
Generic HolProof Source #
Instance details Associated Types type Rep HolProof :: Type -> Type Methods from :: HolProof -> Rep HolProof x to :: Rep HolProof x -> HolProof
Generic HolType Source #
Instance details Associated Types type Rep HolType :: Type -> Type Methods from :: HolType -> Rep HolType x to :: Rep HolType x -> HolType
Generic Sign Source #
Instance details Associated Types type Rep Sign :: Type -> Type Methods from :: Sign -> Rep Sign x to :: Rep Sign x -> Sign
Generic Sentence Source #
Instance details Associated Types type Rep Sentence :: Type -> Type Methods from :: Sentence -> Rep Sentence x to :: Rep Sentence x -> Sentence
FromJSON HolLightSL Source #
Instance details Methods parseJSON :: Value -> Parser HolLightSL parseJSONList :: Value -> Parser [HolLightSL]
FromJSON Term Source #
Instance details Methods parseJSON :: Value -> Parser Term parseJSONList :: Value -> Parser [Term]
FromJSON HolTermInfo Source #
Instance details Methods parseJSON :: Value -> Parser HolTermInfo parseJSONList :: Value -> Parser [HolTermInfo]
FromJSON HolParseType Source #
Instance details Methods parseJSON :: Value -> Parser HolParseType parseJSONList :: Value -> Parser [HolParseType]
FromJSON HolProof Source #
Instance details Methods parseJSON :: Value -> Parser HolProof parseJSONList :: Value -> Parser [HolProof]
FromJSON HolType Source #
Instance details Methods parseJSON :: Value -> Parser HolType parseJSONList :: Value -> Parser [HolType]
FromJSON Sign Source #
Instance details Methods parseJSON :: Value -> Parser Sign parseJSONList :: Value -> Parser [Sign]
FromJSON Sentence Source #
Instance details Methods parseJSON :: Value -> Parser Sentence parseJSONList :: Value -> Parser [Sentence]
ToJSON HolLightSL Source #
Instance details Methods toJSON :: HolLightSL -> Value toEncoding :: HolLightSL -> Encoding toJSONList :: [HolLightSL] -> Value toEncodingList :: [HolLightSL] -> Encoding
ToJSON Term Source #
Instance details Methods toJSON :: Term -> Value toEncoding :: Term -> Encoding toJSONList :: [Term] -> Value toEncodingList :: [Term] -> Encoding
ToJSON HolTermInfo Source #
Instance details Methods toJSON :: HolTermInfo -> Value toEncoding :: HolTermInfo -> Encoding toJSONList :: [HolTermInfo] -> Value toEncodingList :: [HolTermInfo] -> Encoding
ToJSON HolParseType Source #
Instance details Methods toJSON :: HolParseType -> Value toEncoding :: HolParseType -> Encoding toJSONList :: [HolParseType] -> Value toEncodingList :: [HolParseType] -> Encoding
ToJSON HolProof Source #
Instance details Methods toJSON :: HolProof -> Value toEncoding :: HolProof -> Encoding toJSONList :: [HolProof] -> Value toEncodingList :: [HolProof] -> Encoding
ToJSON HolType Source #
Instance details Methods toJSON :: HolType -> Value toEncoding :: HolType -> Encoding toJSONList :: [HolType] -> Value toEncodingList :: [HolType] -> Encoding
ToJSON Sign Source #
Instance details Methods toJSON :: Sign -> Value toEncoding :: Sign -> Encoding toJSONList :: [Sign] -> Value toEncodingList :: [Sign] -> Encoding
ToJSON Sentence Source #
Instance details Methods toJSON :: Sentence -> Value toEncoding :: Sentence -> Encoding toJSONList :: [Sentence] -> Value toEncodingList :: [Sentence] -> Encoding
ShATermConvertible HolLightSL Source #
Instance details Methods toShATermAux :: ATermTable -> HolLightSL -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [HolLightSL] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, HolLightSL) fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolLightSL])
ShATermConvertible Term Source #
Instance details Methods toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Term] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Term) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Term])
ShATermConvertible HolTermInfo Source #
Instance details Methods toShATermAux :: ATermTable -> HolTermInfo -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [HolTermInfo] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, HolTermInfo) fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolTermInfo])
ShATermConvertible HolParseType Source #
Instance details Methods toShATermAux :: ATermTable -> HolParseType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [HolParseType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, HolParseType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolParseType])
ShATermConvertible HolProof Source #
Instance details Methods toShATermAux :: ATermTable -> HolProof -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [HolProof] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, HolProof) fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolProof])
ShATermConvertible HolType Source #
Instance details Methods toShATermAux :: ATermTable -> HolType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [HolType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, HolType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolType])
ShATermConvertible Sign Source #
Instance details Methods toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sign] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign])
ShATermConvertible Sentence Source #
Instance details Methods toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sentence] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sentence) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sentence])