Hets - the Heterogeneous Tool Set

Copyright	(c) Jonathan von Schroeder, DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	jonathan.von_schroeder@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred

HolLight.Term

Description

Definition of terms for HolLight logic

Ref.

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

Documentation

Constructors

TyVar String
TyApp String [HolType]

Instances

Eq HolType
Data HolType
Ord HolType
Read HolType
Show HolType
ShATermConvertible HolType
Typeable * HolType

Constructors

Instances

Eq HolProof
Data HolProof
Ord HolProof
Show HolProof
ShATermConvertible HolProof
Typeable * HolProof

data HolParseType

Constructors

Normal
PrefixT
InfixL Int
InfixR Int
Binder

Instances

Eq HolParseType
Data HolParseType
Ord HolParseType
Read HolParseType
Show HolParseType
ShATermConvertible HolParseType
Typeable * HolParseType

data HolTermInfo

Constructors

HolTermInfo (HolParseType, Maybe (String, HolParseType))

Instances

Eq HolTermInfo
Data HolTermInfo
Ord HolTermInfo
Read HolTermInfo
Show HolTermInfo
ShATermConvertible HolTermInfo
Typeable * HolTermInfo

data Term

Constructors

Var String HolType HolTermInfo
Const String HolType HolTermInfo
Comb Term Term
Abs Term Term

Instances

Eq Term
Data Term
Ord Term
Read Term
Show Term
ShATermConvertible Term
Typeable * Term