-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Higher order logic
--   
--   This package implements a higher order logic kernel with OpenTheory
--   support.
@package hol
@version 1.3


module HOL.Util
mkUnsafe :: String -> Maybe a -> a
mkUnsafe1 :: String -> (a -> Maybe b) -> a -> b
mkUnsafe2 :: String -> (a -> b -> Maybe c) -> a -> b -> c


module HOL.Name
newtype Namespace
Namespace :: [String] -> Namespace
data Name
Name :: Namespace -> String -> Name
global :: Namespace
mkGlobal :: String -> Name
destGlobal :: Name -> Maybe String
isGlobal :: Name -> Bool
variantAvoiding :: Set Name -> Name -> Name
boolNamespace :: Namespace
listNamespace :: Namespace
pairNamespace :: Namespace
sumNamespace :: Namespace
functionNamespace :: Namespace
naturalNamespace :: Namespace
realNamespace :: Namespace
setNamespace :: Namespace
instance GHC.Show.Show HOL.Name.Name
instance GHC.Classes.Ord HOL.Name.Name
instance GHC.Classes.Eq HOL.Name.Name
instance GHC.Show.Show HOL.Name.Namespace
instance GHC.Classes.Ord HOL.Name.Namespace
instance GHC.Classes.Eq HOL.Name.Namespace


module HOL.Parse
spaceParser :: Parsec Text st ()
eolParser :: Parsec Text st ()
lineParser :: Parsec Text st Char
class Parsable a where fromText t = case parse (parser <* eof) "" t of { Left _ -> Nothing Right a -> Just a } fromString = fromText . pack fromStringUnsafe s = case fromString s of { Just a -> a Nothing -> error $ "couldn't parse " ++ show s } fromTextFile file = do { bs <- readFile file; let txt = decodeUtf8 bs; case parse (parser <* eof) file txt of { Left e -> error $ show e Right a -> return a } }
parser :: Parsable a => Parsec Text st a
fromText :: Parsable a => Text -> Maybe a
fromString :: Parsable a => String -> Maybe a
fromStringUnsafe :: Parsable a => String -> a
fromTextFile :: Parsable a => FilePath -> IO a
data ParseInteger
StartParseInteger :: ParseInteger
ZeroParseInteger :: ParseInteger
NegativeParseInteger :: ParseInteger
NonZeroParseInteger :: Bool -> !Integer -> ParseInteger
ErrorParseInteger :: ParseInteger
advanceParseInteger :: ParseInteger -> Char -> ParseInteger
endParseInteger :: ParseInteger -> Maybe Integer
type FoldlParseInteger a = (ParseInteger -> Char -> ParseInteger) -> ParseInteger -> a -> ParseInteger
parseInteger :: FoldlParseInteger a -> a -> Maybe Integer
instance HOL.Parse.Parsable GHC.Integer.Type.Integer
instance HOL.Parse.Parsable HOL.Name.Name


module HOL.Data
type Size = Integer
data TypeVar
TypeVar :: Name -> TypeVar
data TypeOp
TypeOp :: Name -> TypeOpProv -> TypeOp
data TypeOpProv
UndefTypeOpProv :: TypeOpProv
DefTypeOpProv :: TypeOpDef -> TypeOpProv
data TypeOpDef
TypeOpDef :: Term -> [TypeVar] -> TypeOpDef
data Type
Type :: TypeData -> TypeId -> Size -> (Set TypeVar) -> Type
data TypeData
VarType :: TypeVar -> TypeData
OpType :: TypeOp -> [Type] -> TypeData
type TypeId = StableName TypeData
data Var
Var :: Name -> Type -> Var
data Const
Const :: Name -> ConstProv -> Const
data ConstProv
UndefConstProv :: ConstProv
DefConstProv :: ConstDef -> ConstProv
AbsConstProv :: TypeOpDef -> ConstProv
RepConstProv :: TypeOpDef -> ConstProv
data ConstDef
ConstDef :: Term -> ConstDef
data Term
Term :: TermData -> TermId -> Size -> Type -> (Set TypeVar) -> (Set Var) -> Term
data TermData
ConstTerm :: Const -> Type -> TermData
VarTerm :: Var -> TermData
AppTerm :: Term -> Term -> TermData
AbsTerm :: Var -> Term -> TermData
type TermId = StableName TermData
instance GHC.Show.Show HOL.Data.ConstDef
instance GHC.Classes.Ord HOL.Data.ConstDef
instance GHC.Classes.Eq HOL.Data.ConstDef
instance GHC.Show.Show HOL.Data.ConstProv
instance GHC.Classes.Ord HOL.Data.ConstProv
instance GHC.Classes.Eq HOL.Data.ConstProv
instance GHC.Show.Show HOL.Data.Const
instance GHC.Classes.Ord HOL.Data.Const
instance GHC.Classes.Eq HOL.Data.Const
instance GHC.Show.Show HOL.Data.TypeOpDef
instance GHC.Classes.Ord HOL.Data.TypeOpDef
instance GHC.Classes.Eq HOL.Data.TypeOpDef
instance GHC.Show.Show HOL.Data.TypeOpProv
instance GHC.Classes.Ord HOL.Data.TypeOpProv
instance GHC.Classes.Eq HOL.Data.TypeOpProv
instance GHC.Show.Show HOL.Data.TypeOp
instance GHC.Classes.Ord HOL.Data.TypeOp
instance GHC.Classes.Eq HOL.Data.TypeOp
instance GHC.Show.Show HOL.Data.TypeData
instance GHC.Classes.Ord HOL.Data.TypeData
instance GHC.Classes.Eq HOL.Data.TypeData
instance GHC.Show.Show HOL.Data.Var
instance GHC.Classes.Ord HOL.Data.Var
instance GHC.Classes.Eq HOL.Data.Var
instance GHC.Show.Show HOL.Data.TermData
instance GHC.Classes.Ord HOL.Data.TermData
instance GHC.Classes.Eq HOL.Data.TermData
instance GHC.Show.Show HOL.Data.TypeVar
instance GHC.Classes.Ord HOL.Data.TypeVar
instance GHC.Classes.Eq HOL.Data.TypeVar
instance GHC.Classes.Eq HOL.Data.Type
instance GHC.Classes.Ord HOL.Data.Type
instance GHC.Show.Show HOL.Data.Type
instance GHC.Classes.Eq HOL.Data.Term
instance GHC.Classes.Ord HOL.Data.Term
instance GHC.Show.Show HOL.Data.Term


module HOL.TypeData
mkVar :: TypeVar -> TypeData
destVar :: TypeData -> Maybe TypeVar
isVar :: TypeData -> Bool
eqVar :: TypeVar -> TypeData -> Bool
mkOp :: TypeOp -> [Type] -> TypeData
destOp :: TypeData -> Maybe (TypeOp, [Type])
isOp :: TypeData -> Bool
destGivenOp :: TypeOp -> TypeData -> Maybe [Type]
isGivenOp :: TypeOp -> TypeData -> Bool
size :: TypeData -> Size
isNullaryOp :: TypeOp -> TypeData -> Bool
destUnaryOp :: TypeOp -> TypeData -> Maybe Type
isUnaryOp :: TypeOp -> TypeData -> Bool
destBinaryOp :: TypeOp -> TypeData -> Maybe (Type, Type)
isBinaryOp :: TypeOp -> TypeData -> Bool


module HOL.TypeOp
name :: TypeOp -> Name
prov :: TypeOp -> TypeOpProv
mkUndef :: Name -> TypeOp
isUndef :: TypeOp -> Bool
class HasOps a
ops :: HasOps a => a -> Set TypeOp
boolName :: Name
bool :: TypeOp
funName :: Name
fun :: TypeOp
indName :: Name
ind :: TypeOp
primitives :: Set TypeOp
productName :: Name
sumName :: Name
naturalName :: Name
instance HOL.TypeOp.HasOps HOL.Data.TypeOp
instance HOL.TypeOp.HasOps a => HOL.TypeOp.HasOps [a]
instance HOL.TypeOp.HasOps a => HOL.TypeOp.HasOps (Data.Set.Base.Set a)
instance HOL.TypeOp.HasOps HOL.Data.TypeData
instance HOL.TypeOp.HasOps HOL.Data.Type
instance HOL.TypeOp.HasOps HOL.Data.Var
instance HOL.TypeOp.HasOps HOL.Data.TermData
instance HOL.TypeOp.HasOps HOL.Data.Term


module HOL.TypeVar
mk :: Name -> TypeVar
dest :: TypeVar -> Name
eqName :: Name -> TypeVar -> Bool
alpha :: TypeVar
beta :: TypeVar
class HasVars a
vars :: HasVars a => a -> Set TypeVar
instance HOL.TypeVar.HasVars HOL.Data.TypeVar
instance HOL.TypeVar.HasVars a => HOL.TypeVar.HasVars [a]
instance HOL.TypeVar.HasVars a => HOL.TypeVar.HasVars (Data.Set.Base.Set a)
instance HOL.TypeVar.HasVars HOL.Data.TypeData
instance HOL.TypeVar.HasVars HOL.Data.Type
instance HOL.TypeVar.HasVars HOL.Data.Var
instance HOL.TypeVar.HasVars HOL.Data.TermData
instance HOL.TypeVar.HasVars HOL.Data.Term


module HOL.Type
dest :: Type -> TypeData
mk :: TypeData -> Type
mkVar :: TypeVar -> Type
destVar :: Type -> Maybe TypeVar
isVar :: Type -> Bool
eqVar :: TypeVar -> Type -> Bool
mkOp :: TypeOp -> [Type] -> Type
destOp :: Type -> Maybe (TypeOp, [Type])
isOp :: Type -> Bool
destGivenOp :: TypeOp -> Type -> Maybe [Type]
isGivenOp :: TypeOp -> Type -> Bool
size :: Type -> Size
isNullaryOp :: TypeOp -> Type -> Bool
destUnaryOp :: TypeOp -> Type -> Maybe Type
isUnaryOp :: TypeOp -> Type -> Bool
destBinaryOp :: TypeOp -> Type -> Maybe (Type, Type)
isBinaryOp :: TypeOp -> Type -> Bool
alpha :: Type
beta :: Type
bool :: Type
isBool :: Type -> Bool
mkPred :: Type -> Type
destPred :: Type -> Maybe Type
isPred :: Type -> Bool
mkRel :: Type -> Type -> Type
destRel :: Type -> Maybe (Type, Type)
isRel :: Type -> Bool
mkFun :: Type -> Type -> Type
destFun :: Type -> Maybe (Type, Type)
isFun :: Type -> Bool
domain :: Type -> Maybe Type
range :: Type -> Maybe Type
listMkFun :: [Type] -> Type -> Type
stripFun :: Type -> ([Type], Type)
ind :: Type
isInd :: Type -> Bool
mkEq :: Type -> Type
destEq :: Type -> Maybe Type
isEq :: Type -> Bool
mkSelect :: Type -> Type
destSelect :: Type -> Maybe Type
isSelect :: Type -> Bool


module HOL.TypeSubst
data TypeSubst
TypeSubst :: (Map TypeVar Type) -> (Map Type (Maybe Type)) -> TypeSubst
mk :: Map TypeVar Type -> TypeSubst
dest :: TypeSubst -> Map TypeVar Type
fromList :: [(TypeVar, Type)] -> TypeSubst
empty :: TypeSubst
singleton :: TypeVar -> Type -> TypeSubst
null :: TypeSubst -> Bool
varSubst :: TypeVar -> TypeSubst -> Maybe Type
dataSubst :: TypeData -> TypeSubst -> (Maybe Type, TypeSubst)
class CanSubst a where sharingSubst x s = if null s then (Nothing, s) else basicSubst x s subst s x = fst $ sharingSubst x s trySharingSubst x s = (fromMaybe x x', s') where (x', s') = sharingSubst x s trySubst s x = fromMaybe x (subst s x)
basicSubst :: CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
sharingSubst :: CanSubst a => a -> TypeSubst -> (Maybe a, TypeSubst)
subst :: CanSubst a => TypeSubst -> a -> Maybe a
trySharingSubst :: CanSubst a => a -> TypeSubst -> (a, TypeSubst)
trySubst :: CanSubst a => TypeSubst -> a -> a

-- | <ul>
--   <li>subst (compose s1 s2) t == subst s2 (subst s1 t)</li>
--   </ul>
compose :: TypeSubst -> TypeSubst -> TypeSubst
instance GHC.Classes.Eq HOL.TypeSubst.TypeSubst
instance HOL.TypeSubst.CanSubst a => HOL.TypeSubst.CanSubst [a]
instance (GHC.Classes.Ord a, HOL.TypeSubst.CanSubst a) => HOL.TypeSubst.CanSubst (Data.Set.Base.Set a)
instance HOL.TypeSubst.CanSubst HOL.Data.Type
instance HOL.TypeSubst.CanSubst HOL.Data.Var


module HOL.Var
mk :: Name -> Type -> Var
dest :: Var -> (Name, Type)
name :: Var -> Name
typeOf :: Var -> Type
class HasFree a where freeIn v x = member v (free x) notFreeIn v x = notMember v (free x) closed = null . free
free :: HasFree a => a -> Set Var
freeIn :: HasFree a => Var -> a -> Bool
notFreeIn :: HasFree a => Var -> a -> Bool
closed :: HasFree a => a -> Bool
renameAvoiding :: Set Name -> Var -> Var
instance HOL.Var.HasFree HOL.Data.Var
instance HOL.Var.HasFree a => HOL.Var.HasFree [a]
instance HOL.Var.HasFree a => HOL.Var.HasFree (Data.Set.Base.Set a)
instance HOL.Var.HasFree HOL.Data.TermData
instance HOL.Var.HasFree HOL.Data.Term


module HOL.TermData
mkConst :: Const -> Type -> TermData
destConst :: TermData -> Maybe (Const, Type)
isConst :: TermData -> Bool
destGivenConst :: Const -> TermData -> Maybe Type
isGivenConst :: Const -> TermData -> Bool
mkVar :: Var -> TermData
destVar :: TermData -> Maybe Var
isVar :: TermData -> Bool
eqVar :: Var -> TermData -> Bool
mkApp :: Term -> Term -> Maybe TermData
destApp :: TermData -> Maybe (Term, Term)
isApp :: TermData -> Bool
mkAbs :: Var -> Term -> TermData
destAbs :: TermData -> Maybe (Var, Term)
isAbs :: TermData -> Bool
size :: TermData -> Size
typeOf :: TermData -> Type


module HOL.Const
name :: Const -> Name
prov :: Const -> ConstProv
mkUndef :: Name -> Const
isUndef :: Const -> Bool
class HasConsts a
consts :: HasConsts a => a -> Set Const
eqName :: Name
eq :: Const
selectName :: Name
select :: Const
primitives :: Set Const
condName :: Name
conjName :: Name
disjName :: Name
existsName :: Name
existsUniqueName :: Name
forallName :: Name
impName :: Name
negName :: Name
appendName :: Name
consName :: Name
pairName :: Name
composeName :: Name
funpowName :: Name
addName :: Name
bit0Name :: Name
bit1Name :: Name
divName :: Name
geName :: Name
gtName :: Name
leName :: Name
ltName :: Name
modName :: Name
multName :: Name
powerName :: Name
subName :: Name
zeroName :: Name
addRealName :: Name
divRealName :: Name
fromNaturalRealName :: Name
geRealName :: Name
gtRealName :: Name
leRealName :: Name
ltRealName :: Name
multRealName :: Name
powerRealName :: Name
subRealName :: Name
crossName :: Name
deleteName :: Name
differenceName :: Name
fromPredicateName :: Name
insertName :: Name
intersectName :: Name
memberName :: Name
properSubsetName :: Name
subsetName :: Name
unionName :: Name
instance HOL.Const.HasConsts HOL.Data.Const
instance HOL.Const.HasConsts a => HOL.Const.HasConsts [a]
instance HOL.Const.HasConsts a => HOL.Const.HasConsts (Data.Set.Base.Set a)
instance HOL.Const.HasConsts HOL.Data.TermData
instance HOL.Const.HasConsts HOL.Data.Term


module HOL.Term
dest :: Term -> TermData
mk :: TermData -> Term
mkConst :: Const -> Type -> Term
destConst :: Term -> Maybe (Const, Type)
isConst :: Term -> Bool
destGivenConst :: Const -> Term -> Maybe Type
isGivenConst :: Const -> Term -> Bool
mkVar :: Var -> Term
destVar :: Term -> Maybe Var
isVar :: Term -> Bool
eqVar :: Var -> Term -> Bool
mkApp :: Term -> Term -> Maybe Term
mkAppUnsafe :: Term -> Term -> Term
destApp :: Term -> Maybe (Term, Term)
isApp :: Term -> Bool
rator :: Term -> Maybe Term
rand :: Term -> Maybe Term
land :: Term -> Maybe Term
listMkApp :: Term -> [Term] -> Maybe Term
listMkAppUnsafe :: Term -> [Term] -> Term
stripApp :: Term -> (Term, [Term])
mkAbs :: Var -> Term -> Term
destAbs :: Term -> Maybe (Var, Term)
isAbs :: Term -> Bool
listMkAbs :: [Var] -> Term -> Term
stripAbs :: Term -> ([Var], Term)
size :: Term -> Size
typeOf :: Term -> Type
isBool :: Term -> Bool
sameType :: Term -> Term -> Bool
sameTypeVar :: Var -> Term -> Bool
alphaCompare :: Term -> Term -> Ordering
alphaEqual :: Term -> Term -> Bool
mkEqConst :: Type -> Term
destEqConst :: Term -> Maybe Type
isEqConst :: Term -> Bool
mkEq :: Term -> Term -> Maybe Term
mkEqUnsafe :: Term -> Term -> Term
destEq :: Term -> Maybe (Term, Term)
isEq :: Term -> Bool
lhs :: Term -> Maybe Term
rhs :: Term -> Maybe Term
rhsUnsafe :: Term -> Term
mkRefl :: Term -> Term
destRefl :: Term -> Maybe Term
isRefl :: Term -> Bool
mkSelectConst :: Type -> Term
destSelectConst :: Term -> Maybe Type
isSelectConst :: Term -> Bool
mkSelect :: Var -> Term -> Term
destSelect :: Term -> Maybe (Var, Term)
isSelect :: Term -> Bool


module HOL.Subst
data Subst
Subst :: TypeSubst -> (Map Var Term) -> (Map Term (Maybe Term)) -> Subst
mk :: TypeSubst -> Map Var Term -> Maybe Subst
mkUnsafe :: TypeSubst -> Map Var Term -> Subst
dest :: Subst -> (TypeSubst, Map Var Term)
fromList :: [(TypeVar, Type)] -> [(Var, Term)] -> Maybe Subst
fromListUnsafe :: [(TypeVar, Type)] -> [(Var, Term)] -> Subst
empty :: Subst
singleton :: Var -> Term -> Maybe Subst
singletonUnsafe :: Var -> Term -> Subst
null :: Subst -> Bool
capturableVars :: Var -> Term -> Term -> Set Var
renameBoundVar :: Var -> Term -> Term -> Term -> Term
avoidCapture :: Bool -> Var -> Var -> Term -> Term -> (Var, Term)
varSubst :: Var -> Subst -> (Maybe Term, Subst)
dataSubst :: TermData -> Subst -> (Maybe Term, Subst)
class CanSubst a where sharingSubst x s = if null s then (Nothing, s) else basicSubst x s subst s x = fst $ sharingSubst x s typeSubst ts = subst $ mkUnsafe ts empty trySharingSubst x s = (fromMaybe x x', s') where (x', s') = sharingSubst x s trySubst s x = fromMaybe x (subst s x) tryTypeSubst ts x = fromMaybe x (typeSubst ts x)
basicSubst :: CanSubst a => a -> Subst -> (Maybe a, Subst)
sharingSubst :: CanSubst a => a -> Subst -> (Maybe a, Subst)
subst :: CanSubst a => Subst -> a -> Maybe a
typeSubst :: CanSubst a => TypeSubst -> a -> Maybe a
trySharingSubst :: CanSubst a => a -> Subst -> (a, Subst)
trySubst :: CanSubst a => Subst -> a -> a
tryTypeSubst :: CanSubst a => TypeSubst -> a -> a
instance HOL.Subst.CanSubst a => HOL.Subst.CanSubst [a]
instance (GHC.Classes.Ord a, HOL.Subst.CanSubst a) => HOL.Subst.CanSubst (Data.Set.Base.Set a)
instance HOL.Subst.CanSubst HOL.Data.Type
instance HOL.Subst.CanSubst HOL.Data.Var
instance HOL.Subst.CanSubst HOL.Data.Term


module HOL.TermAlpha
newtype TermAlpha
TermAlpha :: Term -> TermAlpha
mk :: Term -> TermAlpha
dest :: TermAlpha -> Term
typeOf :: TermAlpha -> Type
isBool :: TermAlpha -> Bool
axiomOfExtensionality :: TermAlpha
axiomOfChoice :: TermAlpha
axiomOfInfinity :: TermAlpha
standardAxioms :: Set TermAlpha
standardAxiomName :: TermAlpha -> String
instance GHC.Show.Show HOL.TermAlpha.TermAlpha
instance GHC.Classes.Eq HOL.TermAlpha.TermAlpha
instance GHC.Classes.Ord HOL.TermAlpha.TermAlpha
instance HOL.TypeVar.HasVars HOL.TermAlpha.TermAlpha
instance HOL.TypeOp.HasOps HOL.TermAlpha.TermAlpha
instance HOL.Const.HasConsts HOL.TermAlpha.TermAlpha
instance HOL.Var.HasFree HOL.TermAlpha.TermAlpha
instance HOL.Subst.CanSubst HOL.TermAlpha.TermAlpha


module HOL.Sequent
data Sequent
Sequent :: TermAlpha -> Set TermAlpha -> Sequent
[concl] :: Sequent -> TermAlpha
[hyp] :: Sequent -> Set TermAlpha
mk :: Set TermAlpha -> TermAlpha -> Maybe Sequent
mkUnsafe :: Set TermAlpha -> TermAlpha -> Sequent
dest :: Sequent -> (Set TermAlpha, TermAlpha)
nullHyp :: Sequent -> Bool
mkNullHyp :: TermAlpha -> Maybe Sequent
mkNullHypUnsafe :: TermAlpha -> Sequent
axiomOfExtensionality :: Sequent
axiomOfChoice :: Sequent
axiomOfInfinity :: Sequent
standardAxioms :: Set Sequent
instance GHC.Show.Show HOL.Sequent.Sequent
instance GHC.Classes.Ord HOL.Sequent.Sequent
instance GHC.Classes.Eq HOL.Sequent.Sequent
instance HOL.TypeVar.HasVars HOL.Sequent.Sequent
instance HOL.TypeOp.HasOps HOL.Sequent.Sequent
instance HOL.Const.HasConsts HOL.Sequent.Sequent
instance HOL.Var.HasFree HOL.Sequent.Sequent
instance HOL.Subst.CanSubst HOL.Sequent.Sequent


module HOL.Thm
data Thm
assume :: Term -> Maybe Thm
axiomOfChoice :: Thm
axiomOfExtensionality :: Thm
axiomOfInfinity :: Thm
betaConv :: Term -> Maybe Thm
concl :: Thm -> TermAlpha
deductAntisym :: Thm -> Thm -> Thm
defineConst :: Name -> Term -> Maybe (Const, Thm)
defineTypeOp :: Name -> Name -> Name -> [TypeVar] -> Thm -> Maybe (TypeOp, Const, Const, Thm, Thm)
dest :: Thm -> Sequent
eqMp :: Thm -> Thm -> Maybe Thm
hyp :: Thm -> Set TermAlpha
mkAbs :: Var -> Thm -> Maybe Thm
mkAbsUnsafe :: Var -> Thm -> Thm
mkApp :: Thm -> Thm -> Maybe Thm
mkAppUnsafe :: Thm -> Thm -> Thm
nullHyp :: Thm -> Bool
refl :: Term -> Thm
standardAxioms :: Set Thm
subst :: Subst -> Thm -> Thm
instance GHC.Show.Show HOL.Thm.Thm
instance GHC.Classes.Ord HOL.Thm.Thm
instance GHC.Classes.Eq HOL.Thm.Thm
instance HOL.TypeVar.HasVars HOL.Thm.Thm
instance HOL.TypeOp.HasOps HOL.Thm.Thm
instance HOL.Const.HasConsts HOL.Thm.Thm
instance HOL.Var.HasFree HOL.Thm.Thm
instance HOL.Subst.CanSubst HOL.Thm.Thm


module HOL.Print
isSymbolChar :: Char -> Bool
isSymbolString :: String -> Bool
ppSymbolName :: Name -> Doc
type PrefixOp = Doc -> Doc
ppPrefixOps :: [PrefixOp] -> Doc -> Doc
type Prec = Int
data Assoc
LeftAssoc :: Assoc
RightAssoc :: Assoc
NonAssoc :: Assoc
type InfixOp = (Prec, Assoc, Doc -> Doc)
ppInfixOps :: (a -> Maybe (InfixOp, a, a)) -> (Bool -> a -> Doc) -> a -> Doc
class Printable a where toStringWith style = renderStyle style . toDoc toString = toStringWith style where style = style {PP.lineLength = 80, PP.ribbonsPerLine = 1.0}
toDoc :: Printable a => a -> Doc
toStringWith :: Printable a => Style -> a -> String
toString :: Printable a => a -> String
quoteNamespace :: Namespace -> Doc
quoteName :: Name -> Doc
instance GHC.Show.Show HOL.Print.Assoc
instance GHC.Classes.Ord HOL.Print.Assoc
instance GHC.Classes.Eq HOL.Print.Assoc
instance HOL.Print.Printable Text.PrettyPrint.HughesPJ.Doc
instance HOL.Print.Printable GHC.Integer.Type.Integer
instance HOL.Print.Printable a => HOL.Print.Printable [a]
instance HOL.Print.Printable a => HOL.Print.Printable (Data.Set.Base.Set a)
instance HOL.Print.Printable HOL.Name.Namespace
instance HOL.Print.Printable HOL.Name.Name
instance HOL.Print.Printable HOL.Data.TypeVar
instance HOL.Print.Printable HOL.Data.TypeOp
instance HOL.Print.Printable HOL.Data.Type
instance HOL.Print.Printable HOL.TypeSubst.TypeSubst
instance HOL.Print.Printable HOL.Data.Const
instance HOL.Print.Printable HOL.Data.Var
instance HOL.Print.Printable HOL.Data.Term
instance HOL.Print.Printable HOL.TermAlpha.TermAlpha
instance HOL.Print.Printable HOL.Sequent.Sequent
instance HOL.Print.Printable HOL.Thm.Thm


module HOL.OpenTheory.Interpret
data Symbol
TypeOpSymbol :: Name -> Symbol
ConstSymbol :: Name -> Symbol
symbolName :: Symbol -> Name
renameSymbol :: Symbol -> Name -> Symbol
data Rename
Rename :: Symbol -> Name -> Rename
destRename :: Rename -> (Symbol, Name)
newtype Renames
Renames :: [Rename] -> Renames
[destRenames] :: Renames -> [Rename]
concatRenames :: [Renames] -> Renames
data Interpret
Interpret :: (Map Symbol Name) -> Interpret
mk :: Map Symbol Name -> Interpret
empty :: Interpret
toRenames :: Interpret -> Renames
fromRenames :: Renames -> Maybe Interpret
fromRenamesUnsafe :: Renames -> Interpret
interpret :: Interpret -> Symbol -> Name
interpretTypeOp :: Interpret -> Name -> Name
interpretConst :: Interpret -> Name -> Name

-- | <ul>
--   <li>interpret (compose i1 i2) s == interpret i2 (interpret i1 s)</li>
--   </ul>
compose :: Interpret -> Interpret -> Interpret
instance GHC.Show.Show HOL.OpenTheory.Interpret.Renames
instance GHC.Classes.Ord HOL.OpenTheory.Interpret.Renames
instance GHC.Classes.Eq HOL.OpenTheory.Interpret.Renames
instance GHC.Show.Show HOL.OpenTheory.Interpret.Rename
instance GHC.Classes.Ord HOL.OpenTheory.Interpret.Rename
instance GHC.Classes.Eq HOL.OpenTheory.Interpret.Rename
instance GHC.Show.Show HOL.OpenTheory.Interpret.Symbol
instance GHC.Classes.Ord HOL.OpenTheory.Interpret.Symbol
instance GHC.Classes.Eq HOL.OpenTheory.Interpret.Symbol
instance HOL.Print.Printable HOL.OpenTheory.Interpret.Symbol
instance HOL.Parse.Parsable HOL.OpenTheory.Interpret.Symbol
instance HOL.Print.Printable HOL.OpenTheory.Interpret.Rename
instance HOL.Parse.Parsable HOL.OpenTheory.Interpret.Rename
instance HOL.Print.Printable HOL.OpenTheory.Interpret.Renames
instance HOL.Parse.Parsable HOL.OpenTheory.Interpret.Renames
instance HOL.Print.Printable HOL.OpenTheory.Interpret.Interpret
instance HOL.Parse.Parsable HOL.OpenTheory.Interpret.Interpret


module HOL.Rule
rator :: Thm -> Term -> Maybe Thm
ratorUnsafe :: Thm -> Term -> Thm
rand :: Term -> Thm -> Maybe Thm
randUnsafe :: Term -> Thm -> Thm
sym :: Thm -> Maybe Thm
trans :: Thm -> Thm -> Maybe Thm
transUnsafe :: Thm -> Thm -> Thm
proveHyp :: Thm -> Thm -> Maybe Thm
alpha :: Term -> Thm -> Maybe Thm
alphaHyp :: Term -> Thm -> Maybe Thm
alphaSequent :: Sequent -> Thm -> Maybe Thm
defineConstList :: [(Name, Var)] -> Thm -> Maybe ([Const], Thm)
defineTypeOpLegacy :: Name -> Name -> Name -> [TypeVar] -> Thm -> Maybe (TypeOp, Const, Const, Thm, Thm)


module HOL.Conv
data Result
Unchanged :: Result
Changed :: Thm -> Result
newtype Conv
Conv :: (Term -> Maybe Result) -> Conv
apply :: Conv -> Term -> Maybe Result
applyData :: Conv -> TermData -> Maybe Result
applyTerm :: Conv -> Term -> Term
fail :: Conv
id :: Conv
beta :: Conv
orelse :: Conv -> Conv -> Conv
thenc :: Conv -> Conv -> Conv
try :: Conv -> Conv
repeat :: Conv -> Conv
sub :: Conv -> Conv
bottomUp :: Conv -> Conv
instance GHC.Show.Show HOL.Conv.Result
instance GHC.Classes.Ord HOL.Conv.Result
instance GHC.Classes.Eq HOL.Conv.Result


module HOL.Theory
data Theory
Theory :: Map Name (Set TypeOp) -> Map Name (Set Const) -> Map Sequent Thm -> Theory
[typeOpMap] :: Theory -> Map Name (Set TypeOp)
[constMap] :: Theory -> Map Name (Set Const)
[thmMap] :: Theory -> Map Sequent Thm
empty :: Theory
fromThmSet :: Set Thm -> Theory
union :: Theory -> Theory -> Theory
unionList :: [Theory] -> Theory
lookupTypeOp :: Theory -> Name -> Maybe TypeOp
lookupConst :: Theory -> Name -> Maybe Const
sequents :: Theory -> Set Sequent
thms :: Theory -> Set Thm
lookupThm :: Theory -> Sequent -> Maybe Thm
standard :: Theory
instance GHC.Show.Show HOL.Theory.Theory
instance GHC.Classes.Ord HOL.Theory.Theory
instance GHC.Classes.Eq HOL.Theory.Theory
instance HOL.TypeOp.HasOps HOL.Theory.Theory
instance HOL.Const.HasConsts HOL.Theory.Theory
instance HOL.Print.Printable HOL.Theory.Theory


module HOL.OpenTheory.Article
newtype Number
Number :: Integer -> Number
data Object
NumberObject :: Number -> Object
NameObject :: Name -> Object
ListObject :: [Object] -> Object
TypeOpObject :: TypeOp -> Object
TypeObject :: Type -> Object
ConstObject :: Const -> Object
VarObject :: Var -> Object
TermObject :: Term -> Object
ThmObject :: Thm -> Object
class Objective a
toObject :: Objective a => a -> Object
fromObject :: Objective a => Object -> Maybe a
sequentObject :: Object -> Object -> Maybe Sequent
pushObject :: Objective a => a -> [Object] -> [Object]
push2Object :: (Objective a, Objective b) => a -> b -> [Object] -> [Object]
push3Object :: (Objective a, Objective b, Objective c) => a -> b -> c -> [Object] -> [Object]
push4Object :: (Objective a, Objective b, Objective c, Objective d) => a -> b -> c -> d -> [Object] -> [Object]
push5Object :: (Objective a, Objective b, Objective c, Objective d, Objective e) => a -> b -> c -> d -> e -> [Object] -> [Object]
popObject :: Objective a => [Object] -> Maybe (a, [Object])
pop2Object :: (Objective a, Objective b) => [Object] -> Maybe (a, b, [Object])
pop3Object :: (Objective a, Objective b, Objective c) => [Object] -> Maybe (a, b, c, [Object])
pop4Object :: (Objective a, Objective b, Objective c, Objective d) => [Object] -> Maybe (a, b, c, d, [Object])
pop5Object :: (Objective a, Objective b, Objective c, Objective d, Objective e) => [Object] -> Maybe (a, b, c, d, e, [Object])
data Command
NumberCommand :: Number -> Command
NameCommand :: Name -> Command
AbsTermCommand :: Command
AbsThmCommand :: Command
AppTermCommand :: Command
AppThmCommand :: Command
AssumeCommand :: Command
AxiomCommand :: Command
BetaConvCommand :: Command
ConsCommand :: Command
ConstCommand :: Command
ConstTermCommand :: Command
DeductAntisymCommand :: Command
DefCommand :: Command
DefineConstCommand :: Command
DefineConstListCommand :: Command
DefineTypeOpCommand :: Command
EqMpCommand :: Command
HdTlCommand :: Command
NilCommand :: Command
OpTypeCommand :: Command
PopCommand :: Command
PragmaCommand :: Command
ProveHypCommand :: Command
RefCommand :: Command
ReflCommand :: Command
RemoveCommand :: Command
SubstCommand :: Command
SymCommand :: Command
ThmCommand :: Command
TransCommand :: Command
TypeOpCommand :: Command
VarCommand :: Command
VarTermCommand :: Command
VarTypeCommand :: Command
VersionCommand :: Command
DefineTypeOpLegacyCommand :: Command
regularCommands :: [(Command, String)]
type Version = Number
supportedCommand :: Version -> Command -> Bool
versionCommand :: Version -> Command -> Maybe Command
data State
State :: [Object] -> Map Number Object -> Set Thm -> State
[stack] :: State -> [Object]
[dict] :: State -> Map Number Object
[theorems] :: State -> Set Thm
pushState :: Objective a => a -> State -> State
push2State :: (Objective a, Objective b) => a -> b -> State -> State
push5State :: (Objective a, Objective b, Objective c, Objective d, Objective e) => a -> b -> c -> d -> e -> State -> State
popState :: Objective a => State -> Maybe (a, State)
pop2State :: (Objective a, Objective b) => State -> Maybe (a, b, State)
pop3State :: (Objective a, Objective b, Objective c) => State -> Maybe (a, b, c, State)
pop5State :: (Objective a, Objective b, Objective c, Objective d, Objective e) => State -> Maybe (a, b, c, d, e, State)
peekState :: Objective a => State -> Maybe a
defState :: Number -> Object -> State -> State
refState :: Number -> State -> Maybe Object
removeState :: Number -> State -> Maybe (Object, State)
thmState :: Thm -> State -> State
initialState :: State
executeCommand :: Theory -> Interpret -> State -> Command -> Maybe State
type LineNumber = Integer
readArticle :: Theory -> Interpret -> FilePath -> IO (Set Thm)
instance GHC.Show.Show HOL.OpenTheory.Article.State
instance GHC.Classes.Ord HOL.OpenTheory.Article.State
instance GHC.Classes.Eq HOL.OpenTheory.Article.State
instance GHC.Show.Show HOL.OpenTheory.Article.Command
instance GHC.Classes.Ord HOL.OpenTheory.Article.Command
instance GHC.Classes.Eq HOL.OpenTheory.Article.Command
instance GHC.Show.Show HOL.OpenTheory.Article.Object
instance GHC.Classes.Ord HOL.OpenTheory.Article.Object
instance GHC.Classes.Eq HOL.OpenTheory.Article.Object
instance GHC.Show.Show HOL.OpenTheory.Article.Number
instance GHC.Classes.Ord HOL.OpenTheory.Article.Number
instance GHC.Classes.Eq HOL.OpenTheory.Article.Number
instance HOL.Print.Printable HOL.OpenTheory.Article.Number
instance HOL.Parse.Parsable HOL.OpenTheory.Article.Number
instance HOL.OpenTheory.Article.Objective HOL.OpenTheory.Article.Object
instance HOL.OpenTheory.Article.Objective HOL.OpenTheory.Article.Number
instance HOL.OpenTheory.Article.Objective HOL.Name.Name
instance HOL.OpenTheory.Article.Objective a => HOL.OpenTheory.Article.Objective [a]
instance HOL.OpenTheory.Article.Objective HOL.Data.TypeOp
instance HOL.OpenTheory.Article.Objective HOL.Data.Type
instance HOL.OpenTheory.Article.Objective HOL.Data.Const
instance HOL.OpenTheory.Article.Objective HOL.Data.Var
instance HOL.OpenTheory.Article.Objective HOL.Data.Term
instance HOL.OpenTheory.Article.Objective HOL.Thm.Thm
instance (HOL.OpenTheory.Article.Objective a, HOL.OpenTheory.Article.Objective b) => HOL.OpenTheory.Article.Objective (a, b)
instance HOL.Print.Printable HOL.OpenTheory.Article.Object
instance HOL.Parse.Parsable HOL.OpenTheory.Article.Command
instance HOL.Print.Printable HOL.OpenTheory.Article.Command
instance HOL.Print.Printable HOL.OpenTheory.Article.State


module HOL.OpenTheory.Package
newtype Name
Name :: String -> Name
[destName] :: Name -> String
newtype Version
Version :: String -> Version
[destVersion] :: Version -> String
data NameVersion
NameVersion :: Name -> Version -> NameVersion
[name] :: NameVersion -> Name
[version] :: NameVersion -> Version
data KeyValue
KeyValue :: Name -> String -> KeyValue
printKeyValue :: Printable a => Name -> a -> KeyValue
matchKeyValue :: Name -> KeyValue -> Maybe String
parseKeyValue :: Parsable a => Name -> KeyValue -> Maybe a
newtype Info
Info :: [KeyValue] -> Info
[destInfo] :: Info -> [KeyValue]
nullInfo :: Info -> Bool
appendInfo :: Info -> Info -> Info
concatInfo :: [Info] -> Info
firstInfo :: (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstGetInfo :: [Info -> Maybe (a, Info)] -> Info -> Maybe (a, Info)
mapGetInfo :: (a -> b) -> (Info -> Maybe (a, Info)) -> Info -> Maybe (b, Info)
maybeGetInfo :: (Info -> Maybe (a, Info)) -> Info -> (Maybe a, Info)
listGetInfo :: (Info -> Maybe (a, Info)) -> Info -> ([a], Info)
class Informative a where fromInfo i = do { (a, i') <- getInfo i; guard $ nullInfo i'; return a }
toInfo :: Informative a => a -> Info
getInfo :: Informative a => Info -> Maybe (a, Info)
fromInfo :: Informative a => Info -> Maybe a
newtype File
File :: FilePath -> File
[destFile] :: File -> FilePath
data Interpretation
Interpret :: Rename -> Interpretation
Interpretation :: File -> Interpretation
readInterpretation :: FilePath -> [Interpretation] -> IO Interpret
data Operation
Article :: File -> Operation
Include :: NameVersion -> Maybe String -> Operation
[package] :: Operation -> NameVersion
[checksum] :: Operation -> Maybe String
Union :: Operation
data Block
Block :: Name -> [Name] -> [Interpretation] -> Operation -> Block
[block] :: Block -> Name
[imports] :: Block -> [Name]
[interpret] :: Block -> [Interpretation]
[operation] :: Block -> Operation
mkBlock :: Name -> Info -> Maybe Block
destBlock :: Block -> (Name, Info)
data Package
Package :: Info -> [Block] -> Package
[information] :: Package -> Info
[source] :: Package -> [Block]
requires :: Package -> [Name]
packageFile :: FilePath -> Name -> FilePath
opentheory :: [String] -> IO String
opentheoryDirectory :: String -> IO FilePath
directory :: Name -> IO FilePath
directoryVersion :: NameVersion -> IO FilePath
newtype Blocks
Blocks :: [Block] -> Blocks
[destBlocks] :: Blocks -> [Block]
mkBlocks :: [Block] -> Blocks
readVersion :: Theory -> Interpret -> NameVersion -> IO Theory
readPackageFile :: Theory -> Interpret -> FilePath -> IO Theory
readPackage :: Theory -> Interpret -> FilePath -> Package -> IO Theory
readBlocks :: Theory -> Interpret -> FilePath -> Blocks -> IO Theory
readBlock :: Theory -> Interpret -> FilePath -> [Theory] -> Block -> IO Theory
newtype Requires
Requires :: (Map Name ([Name], FilePath, Blocks)) -> Requires
emptyRequires :: Requires
addRequires :: Requires -> Name -> IO Requires
fromListRequires :: [Name] -> IO Requires
readList :: [Name] -> IO [Theory]
instance GHC.Show.Show HOL.OpenTheory.Package.Blocks
instance GHC.Classes.Ord HOL.OpenTheory.Package.Blocks
instance GHC.Classes.Eq HOL.OpenTheory.Package.Blocks
instance GHC.Show.Show HOL.OpenTheory.Package.Package
instance GHC.Classes.Ord HOL.OpenTheory.Package.Package
instance GHC.Classes.Eq HOL.OpenTheory.Package.Package
instance GHC.Show.Show HOL.OpenTheory.Package.Block
instance GHC.Classes.Ord HOL.OpenTheory.Package.Block
instance GHC.Classes.Eq HOL.OpenTheory.Package.Block
instance GHC.Show.Show HOL.OpenTheory.Package.Operation
instance GHC.Classes.Ord HOL.OpenTheory.Package.Operation
instance GHC.Classes.Eq HOL.OpenTheory.Package.Operation
instance GHC.Show.Show HOL.OpenTheory.Package.Interpretation
instance GHC.Classes.Ord HOL.OpenTheory.Package.Interpretation
instance GHC.Classes.Eq HOL.OpenTheory.Package.Interpretation
instance GHC.Show.Show HOL.OpenTheory.Package.File
instance GHC.Classes.Ord HOL.OpenTheory.Package.File
instance GHC.Classes.Eq HOL.OpenTheory.Package.File
instance GHC.Show.Show HOL.OpenTheory.Package.Info
instance GHC.Classes.Ord HOL.OpenTheory.Package.Info
instance GHC.Classes.Eq HOL.OpenTheory.Package.Info
instance GHC.Show.Show HOL.OpenTheory.Package.KeyValue
instance GHC.Classes.Ord HOL.OpenTheory.Package.KeyValue
instance GHC.Classes.Eq HOL.OpenTheory.Package.KeyValue
instance GHC.Show.Show HOL.OpenTheory.Package.NameVersion
instance GHC.Classes.Ord HOL.OpenTheory.Package.NameVersion
instance GHC.Classes.Eq HOL.OpenTheory.Package.NameVersion
instance GHC.Show.Show HOL.OpenTheory.Package.Version
instance GHC.Classes.Ord HOL.OpenTheory.Package.Version
instance GHC.Classes.Eq HOL.OpenTheory.Package.Version
instance GHC.Show.Show HOL.OpenTheory.Package.Name
instance GHC.Classes.Ord HOL.OpenTheory.Package.Name
instance GHC.Classes.Eq HOL.OpenTheory.Package.Name
instance HOL.Print.Printable HOL.OpenTheory.Package.Name
instance HOL.Parse.Parsable HOL.OpenTheory.Package.Name
instance HOL.Print.Printable HOL.OpenTheory.Package.Version
instance HOL.Parse.Parsable HOL.OpenTheory.Package.Version
instance HOL.Print.Printable HOL.OpenTheory.Package.NameVersion
instance HOL.Parse.Parsable HOL.OpenTheory.Package.NameVersion
instance HOL.Print.Printable HOL.OpenTheory.Package.KeyValue
instance HOL.Parse.Parsable HOL.OpenTheory.Package.KeyValue
instance HOL.Print.Printable HOL.OpenTheory.Package.Info
instance HOL.Parse.Parsable HOL.OpenTheory.Package.Info
instance HOL.OpenTheory.Package.Informative a => HOL.OpenTheory.Package.Informative [a]
instance (HOL.OpenTheory.Package.Informative a, HOL.OpenTheory.Package.Informative b) => HOL.OpenTheory.Package.Informative (a, b)
instance HOL.Print.Printable HOL.OpenTheory.Package.File
instance HOL.Parse.Parsable HOL.OpenTheory.Package.File
instance HOL.OpenTheory.Package.Informative HOL.OpenTheory.Package.Interpretation
instance HOL.OpenTheory.Package.Informative HOL.OpenTheory.Package.Operation
instance HOL.Print.Printable HOL.OpenTheory.Package.Block
instance HOL.Parse.Parsable HOL.OpenTheory.Package.Block
instance HOL.Print.Printable HOL.OpenTheory.Package.Package
instance HOL.Parse.Parsable HOL.OpenTheory.Package.Package


module HOL.OpenTheory
readArticle :: Theory -> Interpret -> FilePath -> IO (Set Thm)
readPackages :: [Name] -> IO [Theory]