Safe Haskell	Safe-Inferred
Language	Haskell2010

HOL.Data

Description

Documentation

type Size = Integer Source #

data TypeVar Source #

Constructors

TypeVar Name

Instances

Instances details

Eq TypeVar Source #
Instance details Defined in HOL.Data Methods (==) :: TypeVar -> TypeVar -> Bool # (/=) :: TypeVar -> TypeVar -> Bool #
Ord TypeVar Source #
Instance details Defined in HOL.Data Methods compare :: TypeVar -> TypeVar -> Ordering # (<) :: TypeVar -> TypeVar -> Bool # (<=) :: TypeVar -> TypeVar -> Bool # (>) :: TypeVar -> TypeVar -> Bool # (>=) :: TypeVar -> TypeVar -> Bool # max :: TypeVar -> TypeVar -> TypeVar # min :: TypeVar -> TypeVar -> TypeVar #
Show TypeVar Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> TypeVar -> ShowS # show :: TypeVar -> String # showList :: [TypeVar] -> ShowS #
HasVars TypeVar Source #
Instance details Defined in HOL.TypeVar Methods vars :: TypeVar -> Set TypeVar Source #
Printable TypeVar Source #
Instance details Defined in HOL.Print Methods toDoc :: TypeVar -> Doc Source # toStringWith :: Style -> TypeVar -> String Source # toString :: TypeVar -> String Source #

data TypeOp Source #

Constructors

TypeOp Name TypeOpProv

Instances

Instances details

Eq TypeOp Source #
Instance details Defined in HOL.Data Methods (==) :: TypeOp -> TypeOp -> Bool # (/=) :: TypeOp -> TypeOp -> Bool #
Ord TypeOp Source #
Instance details Defined in HOL.Data Methods compare :: TypeOp -> TypeOp -> Ordering # (<) :: TypeOp -> TypeOp -> Bool # (<=) :: TypeOp -> TypeOp -> Bool # (>) :: TypeOp -> TypeOp -> Bool # (>=) :: TypeOp -> TypeOp -> Bool # max :: TypeOp -> TypeOp -> TypeOp # min :: TypeOp -> TypeOp -> TypeOp #
Show TypeOp Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> TypeOp -> ShowS # show :: TypeOp -> String # showList :: [TypeOp] -> ShowS #
HasOps TypeOp Source #
Instance details Defined in HOL.TypeOp Methods ops :: TypeOp -> Set TypeOp Source #
Printable TypeOp Source #
Instance details Defined in HOL.Print Methods toDoc :: TypeOp -> Doc Source # toStringWith :: Style -> TypeOp -> String Source # toString :: TypeOp -> String Source #
Objective TypeOp Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: TypeOp -> Object Source # fromObject :: Object -> Maybe TypeOp Source #

data TypeOpProv Source #

Constructors

UndefTypeOpProv
DefTypeOpProv TypeOpDef

Instances

Instances details

Eq TypeOpProv Source #
Instance details Defined in HOL.Data Methods (==) :: TypeOpProv -> TypeOpProv -> Bool # (/=) :: TypeOpProv -> TypeOpProv -> Bool #
Ord TypeOpProv Source #
Instance details Defined in HOL.Data Methods compare :: TypeOpProv -> TypeOpProv -> Ordering # (<) :: TypeOpProv -> TypeOpProv -> Bool # (<=) :: TypeOpProv -> TypeOpProv -> Bool # (>) :: TypeOpProv -> TypeOpProv -> Bool # (>=) :: TypeOpProv -> TypeOpProv -> Bool # max :: TypeOpProv -> TypeOpProv -> TypeOpProv # min :: TypeOpProv -> TypeOpProv -> TypeOpProv #
Show TypeOpProv Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> TypeOpProv -> ShowS # show :: TypeOpProv -> String # showList :: [TypeOpProv] -> ShowS #

data TypeOpDef Source #

Constructors

TypeOpDef Term [TypeVar]

Instances

Instances details

Eq TypeOpDef Source #
Instance details Defined in HOL.Data Methods (==) :: TypeOpDef -> TypeOpDef -> Bool # (/=) :: TypeOpDef -> TypeOpDef -> Bool #
Ord TypeOpDef Source #
Instance details Defined in HOL.Data Methods compare :: TypeOpDef -> TypeOpDef -> Ordering # (<) :: TypeOpDef -> TypeOpDef -> Bool # (<=) :: TypeOpDef -> TypeOpDef -> Bool # (>) :: TypeOpDef -> TypeOpDef -> Bool # (>=) :: TypeOpDef -> TypeOpDef -> Bool # max :: TypeOpDef -> TypeOpDef -> TypeOpDef # min :: TypeOpDef -> TypeOpDef -> TypeOpDef #
Show TypeOpDef Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> TypeOpDef -> ShowS # show :: TypeOpDef -> String # showList :: [TypeOpDef] -> ShowS #

data Type Source #

Constructors

Type TypeData TypeId Size (Set TypeVar)

Instances

Instances details

Eq Type Source #
Instance details Defined in HOL.Data Methods (==) :: Type -> Type -> Bool # (/=) :: Type -> Type -> Bool #
Ord Type Source #
Instance details Defined in HOL.Data Methods compare :: Type -> Type -> Ordering # (<) :: Type -> Type -> Bool # (<=) :: Type -> Type -> Bool # (>) :: Type -> Type -> Bool # (>=) :: Type -> Type -> Bool # max :: Type -> Type -> Type # min :: Type -> Type -> Type #
Show Type Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
HasOps Type Source #
Instance details Defined in HOL.TypeOp Methods ops :: Type -> Set TypeOp Source #
HasVars Type Source #
Instance details Defined in HOL.TypeVar Methods vars :: Type -> Set TypeVar Source #
CanSubst Type Source #
Instance details Defined in HOL.TypeSubst Methods basicSubst :: Type -> TypeSubst -> (Maybe Type, TypeSubst) Source # sharingSubst :: Type -> TypeSubst -> (Maybe Type, TypeSubst) Source # subst :: TypeSubst -> Type -> Maybe Type Source # trySharingSubst :: Type -> TypeSubst -> (Type, TypeSubst) Source # trySubst :: TypeSubst -> Type -> Type Source #
CanSubst Type Source #
Instance details Defined in HOL.Subst Methods basicSubst :: Type -> Subst -> (Maybe Type, Subst) Source # sharingSubst :: Type -> Subst -> (Maybe Type, Subst) Source # subst :: Subst -> Type -> Maybe Type Source # typeSubst :: TypeSubst -> Type -> Maybe Type Source # trySharingSubst :: Type -> Subst -> (Type, Subst) Source # trySubst :: Subst -> Type -> Type Source # tryTypeSubst :: TypeSubst -> Type -> Type Source #
Printable Type Source #
Instance details Defined in HOL.Print Methods toDoc :: Type -> Doc Source # toStringWith :: Style -> Type -> String Source # toString :: Type -> String Source #
Objective Type Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Type -> Object Source # fromObject :: Object -> Maybe Type Source #

data TypeData Source #

Constructors

VarType TypeVar
OpType TypeOp [Type]

Instances

Instances details

Eq TypeData Source #
Instance details Defined in HOL.Data Methods (==) :: TypeData -> TypeData -> Bool # (/=) :: TypeData -> TypeData -> Bool #
Ord TypeData Source #
Instance details Defined in HOL.Data Methods compare :: TypeData -> TypeData -> Ordering # (<) :: TypeData -> TypeData -> Bool # (<=) :: TypeData -> TypeData -> Bool # (>) :: TypeData -> TypeData -> Bool # (>=) :: TypeData -> TypeData -> Bool # max :: TypeData -> TypeData -> TypeData # min :: TypeData -> TypeData -> TypeData #
Show TypeData Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> TypeData -> ShowS # show :: TypeData -> String # showList :: [TypeData] -> ShowS #
HasOps TypeData Source #
Instance details Defined in HOL.TypeOp Methods ops :: TypeData -> Set TypeOp Source #
HasVars TypeData Source #
Instance details Defined in HOL.TypeVar Methods vars :: TypeData -> Set TypeVar Source #

type TypeId = StableName TypeData Source #

data Var Source #

Constructors

Var Name Type

Instances

Instances details

Eq Var Source #
Instance details Defined in HOL.Data Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Ord Var Source #
Instance details Defined in HOL.Data Methods compare :: Var -> Var -> Ordering # (<) :: Var -> Var -> Bool # (<=) :: Var -> Var -> Bool # (>) :: Var -> Var -> Bool # (>=) :: Var -> Var -> Bool # max :: Var -> Var -> Var # min :: Var -> Var -> Var #
Show Var Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #
HasOps Var Source #
Instance details Defined in HOL.TypeOp Methods ops :: Var -> Set TypeOp Source #
HasVars Var Source #
Instance details Defined in HOL.TypeVar Methods vars :: Var -> Set TypeVar Source #
CanSubst Var Source #
Instance details Defined in HOL.TypeSubst Methods basicSubst :: Var -> TypeSubst -> (Maybe Var, TypeSubst) Source # sharingSubst :: Var -> TypeSubst -> (Maybe Var, TypeSubst) Source # subst :: TypeSubst -> Var -> Maybe Var Source # trySharingSubst :: Var -> TypeSubst -> (Var, TypeSubst) Source # trySubst :: TypeSubst -> Var -> Var Source #
HasFree Var Source #
Instance details Defined in HOL.Var Methods free :: Var -> Set Var Source # freeIn :: Var -> Var -> Bool Source # notFreeIn :: Var -> Var -> Bool Source # closed :: Var -> Bool Source #
CanSubst Var Source #
Instance details Defined in HOL.Subst Methods basicSubst :: Var -> Subst -> (Maybe Var, Subst) Source # sharingSubst :: Var -> Subst -> (Maybe Var, Subst) Source # subst :: Subst -> Var -> Maybe Var Source # typeSubst :: TypeSubst -> Var -> Maybe Var Source # trySharingSubst :: Var -> Subst -> (Var, Subst) Source # trySubst :: Subst -> Var -> Var Source # tryTypeSubst :: TypeSubst -> Var -> Var Source #
Printable Var Source #
Instance details Defined in HOL.Print Methods toDoc :: Var -> Doc Source # toStringWith :: Style -> Var -> String Source # toString :: Var -> String Source #
Objective Var Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Var -> Object Source # fromObject :: Object -> Maybe Var Source #

data Const Source #

Constructors

Const Name ConstProv

Instances

Instances details

Eq Const Source #
Instance details Defined in HOL.Data Methods (==) :: Const -> Const -> Bool # (/=) :: Const -> Const -> Bool #
Ord Const Source #
Instance details Defined in HOL.Data Methods compare :: Const -> Const -> Ordering # (<) :: Const -> Const -> Bool # (<=) :: Const -> Const -> Bool # (>) :: Const -> Const -> Bool # (>=) :: Const -> Const -> Bool # max :: Const -> Const -> Const # min :: Const -> Const -> Const #
Show Const Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> Const -> ShowS # show :: Const -> String # showList :: [Const] -> ShowS #
HasConsts Const Source #
Instance details Defined in HOL.Const Methods consts :: Const -> Set Const Source #
Printable Const Source #
Instance details Defined in HOL.Print Methods toDoc :: Const -> Doc Source # toStringWith :: Style -> Const -> String Source # toString :: Const -> String Source #
Objective Const Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Const -> Object Source # fromObject :: Object -> Maybe Const Source #

data ConstProv Source #

Constructors

UndefConstProv
DefConstProv ConstDef
AbsConstProv TypeOpDef
RepConstProv TypeOpDef

Instances

Instances details

Eq ConstProv Source #
Instance details Defined in HOL.Data Methods (==) :: ConstProv -> ConstProv -> Bool # (/=) :: ConstProv -> ConstProv -> Bool #
Ord ConstProv Source #
Instance details Defined in HOL.Data Methods compare :: ConstProv -> ConstProv -> Ordering # (<) :: ConstProv -> ConstProv -> Bool # (<=) :: ConstProv -> ConstProv -> Bool # (>) :: ConstProv -> ConstProv -> Bool # (>=) :: ConstProv -> ConstProv -> Bool # max :: ConstProv -> ConstProv -> ConstProv # min :: ConstProv -> ConstProv -> ConstProv #
Show ConstProv Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> ConstProv -> ShowS # show :: ConstProv -> String # showList :: [ConstProv] -> ShowS #

data ConstDef Source #

Constructors

ConstDef Term

Instances

Instances details

Eq ConstDef Source #
Instance details Defined in HOL.Data Methods (==) :: ConstDef -> ConstDef -> Bool # (/=) :: ConstDef -> ConstDef -> Bool #
Ord ConstDef Source #
Instance details Defined in HOL.Data Methods compare :: ConstDef -> ConstDef -> Ordering # (<) :: ConstDef -> ConstDef -> Bool # (<=) :: ConstDef -> ConstDef -> Bool # (>) :: ConstDef -> ConstDef -> Bool # (>=) :: ConstDef -> ConstDef -> Bool # max :: ConstDef -> ConstDef -> ConstDef # min :: ConstDef -> ConstDef -> ConstDef #
Show ConstDef Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> ConstDef -> ShowS # show :: ConstDef -> String # showList :: [ConstDef] -> ShowS #

data Term Source #

Constructors

Term TermData TermId Size Type (Set TypeVar) (Set Var)

Instances

Instances details

Eq Term Source #
Instance details Defined in HOL.Data Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #
Ord Term Source #
Instance details Defined in HOL.Data 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 #
Show Term Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
HasConsts Term Source #
Instance details Defined in HOL.Const Methods consts :: Term -> Set Const Source #
HasOps Term Source #
Instance details Defined in HOL.TypeOp Methods ops :: Term -> Set TypeOp Source #
HasVars Term Source #
Instance details Defined in HOL.TypeVar Methods vars :: Term -> Set TypeVar Source #
HasFree Term Source #
Instance details Defined in HOL.Var Methods free :: Term -> Set Var Source # freeIn :: Var -> Term -> Bool Source # notFreeIn :: Var -> Term -> Bool Source # closed :: Term -> Bool Source #
CanSubst Term Source #
Instance details Defined in HOL.Subst Methods basicSubst :: Term -> Subst -> (Maybe Term, Subst) Source # sharingSubst :: Term -> Subst -> (Maybe Term, Subst) Source # subst :: Subst -> Term -> Maybe Term Source # typeSubst :: TypeSubst -> Term -> Maybe Term Source # trySharingSubst :: Term -> Subst -> (Term, Subst) Source # trySubst :: Subst -> Term -> Term Source # tryTypeSubst :: TypeSubst -> Term -> Term Source #
Printable Term Source #
Instance details Defined in HOL.Print Methods toDoc :: Term -> Doc Source # toStringWith :: Style -> Term -> String Source # toString :: Term -> String Source #
Objective Term Source #
Instance details Defined in HOL.OpenTheory.Article Methods toObject :: Term -> Object Source # fromObject :: Object -> Maybe Term Source #

data TermData Source #

Constructors

ConstTerm Const Type
VarTerm Var
AppTerm Term Term
AbsTerm Var Term

Instances

Instances details

Eq TermData Source #
Instance details Defined in HOL.Data Methods (==) :: TermData -> TermData -> Bool # (/=) :: TermData -> TermData -> Bool #
Ord TermData Source #
Instance details Defined in HOL.Data Methods compare :: TermData -> TermData -> Ordering # (<) :: TermData -> TermData -> Bool # (<=) :: TermData -> TermData -> Bool # (>) :: TermData -> TermData -> Bool # (>=) :: TermData -> TermData -> Bool # max :: TermData -> TermData -> TermData # min :: TermData -> TermData -> TermData #
Show TermData Source #
Instance details Defined in HOL.Data Methods showsPrec :: Int -> TermData -> ShowS # show :: TermData -> String # showList :: [TermData] -> ShowS #
HasConsts TermData Source #
Instance details Defined in HOL.Const Methods consts :: TermData -> Set Const Source #
HasOps TermData Source #
Instance details Defined in HOL.TypeOp Methods ops :: TermData -> Set TypeOp Source #
HasVars TermData Source #
Instance details Defined in HOL.TypeVar Methods vars :: TermData -> Set TypeVar Source #
HasFree TermData Source #
Instance details Defined in HOL.Var Methods free :: TermData -> Set Var Source # freeIn :: Var -> TermData -> Bool Source # notFreeIn :: Var -> TermData -> Bool Source # closed :: TermData -> Bool Source #

type TermId = StableName TermData Source #