Hets - the Heterogeneous Tool Set

Copyright(c) Jonathan von Schroeder DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerjonathan.von_schroeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

HolLight.Term

Description

Definition of terms for HolLight logic

Ref.

http://www.cl.cam.ac.uk/~jrh13/hol-light/

Documentation

data HolType Source #

Constructors

TyVar String 
TyApp String [HolType] 

Instances

Eq HolType Source # 

Methods

(==) :: HolType -> HolType -> Bool

(/=) :: HolType -> HolType -> Bool

Data HolType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HolType -> c HolType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HolType

toConstr :: HolType -> Constr

dataTypeOf :: HolType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c HolType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolType)

gmapT :: (forall b. Data b => b -> b) -> HolType -> HolType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HolType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HolType -> r

gmapQ :: (forall d. Data d => d -> u) -> HolType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HolType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HolType -> m HolType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HolType -> m HolType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HolType -> m HolType

Ord HolType Source # 

Methods

compare :: HolType -> HolType -> Ordering

(<) :: HolType -> HolType -> Bool

(<=) :: HolType -> HolType -> Bool

(>) :: HolType -> HolType -> Bool

(>=) :: HolType -> HolType -> Bool

max :: HolType -> HolType -> HolType

min :: HolType -> HolType -> HolType

Read HolType Source # 

Methods

readsPrec :: Int -> ReadS HolType

readList :: ReadS [HolType]

readPrec :: ReadPrec HolType

readListPrec :: ReadPrec [HolType]

Show HolType Source # 

Methods

showsPrec :: Int -> HolType -> ShowS

show :: HolType -> String

showList :: [HolType] -> ShowS

data HolProof Source #

Constructors

NoProof 

Instances

Eq HolProof Source # 

Methods

(==) :: HolProof -> HolProof -> Bool

(/=) :: HolProof -> HolProof -> Bool

Data HolProof Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HolProof -> c HolProof

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HolProof

toConstr :: HolProof -> Constr

dataTypeOf :: HolProof -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c HolProof)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolProof)

gmapT :: (forall b. Data b => b -> b) -> HolProof -> HolProof

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HolProof -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HolProof -> r

gmapQ :: (forall d. Data d => d -> u) -> HolProof -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HolProof -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HolProof -> m HolProof

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HolProof -> m HolProof

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HolProof -> m HolProof

Ord HolProof Source # 

Methods

compare :: HolProof -> HolProof -> Ordering

(<) :: HolProof -> HolProof -> Bool

(<=) :: HolProof -> HolProof -> Bool

(>) :: HolProof -> HolProof -> Bool

(>=) :: HolProof -> HolProof -> Bool

max :: HolProof -> HolProof -> HolProof

min :: HolProof -> HolProof -> HolProof

Show HolProof Source # 

Methods

showsPrec :: Int -> HolProof -> ShowS

show :: HolProof -> String

showList :: [HolProof] -> ShowS

data HolParseType Source #

Constructors

Normal 
PrefixT 
InfixL Int 
InfixR Int 
Binder 

Instances

Eq HolParseType Source # 

Methods

(==) :: HolParseType -> HolParseType -> Bool

(/=) :: HolParseType -> HolParseType -> Bool

Data HolParseType Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HolParseType -> c HolParseType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HolParseType

toConstr :: HolParseType -> Constr

dataTypeOf :: HolParseType -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c HolParseType)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolParseType)

gmapT :: (forall b. Data b => b -> b) -> HolParseType -> HolParseType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HolParseType -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HolParseType -> r

gmapQ :: (forall d. Data d => d -> u) -> HolParseType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HolParseType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HolParseType -> m HolParseType

Ord HolParseType Source # 
Read HolParseType Source # 

Methods

readsPrec :: Int -> ReadS HolParseType

readList :: ReadS [HolParseType]

readPrec :: ReadPrec HolParseType

readListPrec :: ReadPrec [HolParseType]

Show HolParseType Source # 

Methods

showsPrec :: Int -> HolParseType -> ShowS

show :: HolParseType -> String

showList :: [HolParseType] -> ShowS

data HolTermInfo Source #

Constructors

HolTermInfo (HolParseType, Maybe (String, HolParseType)) 

Instances

Eq HolTermInfo Source # 

Methods

(==) :: HolTermInfo -> HolTermInfo -> Bool

(/=) :: HolTermInfo -> HolTermInfo -> Bool

Data HolTermInfo Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HolTermInfo -> c HolTermInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HolTermInfo

toConstr :: HolTermInfo -> Constr

dataTypeOf :: HolTermInfo -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c HolTermInfo)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HolTermInfo)

gmapT :: (forall b. Data b => b -> b) -> HolTermInfo -> HolTermInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HolTermInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> HolTermInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HolTermInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HolTermInfo -> m HolTermInfo

Ord HolTermInfo Source # 
Read HolTermInfo Source # 

Methods

readsPrec :: Int -> ReadS HolTermInfo

readList :: ReadS [HolTermInfo]

readPrec :: ReadPrec HolTermInfo

readListPrec :: ReadPrec [HolTermInfo]

Show HolTermInfo Source # 

Methods

showsPrec :: Int -> HolTermInfo -> ShowS

show :: HolTermInfo -> String

showList :: [HolTermInfo] -> ShowS

data Term Source #

Instances

Eq Term Source # 

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Data Term Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term

toConstr :: Term -> Constr

dataTypeOf :: Term -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Term)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)

gmapT :: (forall b. Data b => b -> b) -> Term -> Term

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

Ord Term Source # 

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Read Term Source # 

Methods

readsPrec :: Int -> ReadS Term

readList :: ReadS [Term]

readPrec :: ReadPrec Term

readListPrec :: ReadPrec [Term]

Show Term Source # 

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS