Hets - the Heterogeneous Tool Set

Copyright(c) DFKI GmbH 2012
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable(derive Typeable instances)
Safe HaskellNone

HolLight.ATC_HolLight

Contents

Description

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

Orphan instances

ShATermConvertible Term Source # 

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 # 

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 # 

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 # 

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 # 

Methods

toShATermAux :: ATermTable -> HolType -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [HolType] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, HolType)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolType])

ShATermConvertible HolLightSL Source # 

Methods

toShATermAux :: ATermTable -> HolLightSL -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [HolLightSL] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, HolLightSL)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [HolLightSL])

ShATermConvertible Sentence Source # 

Methods

toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sentence] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sentence)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sentence])

ShATermConvertible Sign Source # 

Methods

toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sign] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign])