hol-1.3: Higher order logic

License	MIT
Maintainer	Joe Leslie-Hurd <joe@gilith.com>
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell98

HOL.Var

Description

Documentation

mk :: Name -> Type -> Var Source #

dest :: Var -> (Name, Type) Source #

name :: Var -> Name Source #

typeOf :: Var -> Type Source #

class HasFree a where Source #

Minimal complete definition

Methods

free :: a -> Set Var Source #

freeIn :: Var -> a -> Bool Source #

notFreeIn :: Var -> a -> Bool Source #

closed :: a -> Bool Source #

Instances

HasFree TermData Source #
Methods free :: TermData -> Set Var Source # freeIn :: Var -> TermData -> Bool Source # notFreeIn :: Var -> TermData -> Bool Source # closed :: TermData -> Bool Source #
HasFree Term Source #
Methods free :: Term -> Set Var Source # freeIn :: Var -> Term -> Bool Source # notFreeIn :: Var -> Term -> Bool Source # closed :: Term -> Bool Source #
HasFree Var Source #
Methods free :: Var -> Set Var Source # freeIn :: Var -> Var -> Bool Source # notFreeIn :: Var -> Var -> Bool Source # closed :: Var -> Bool Source #
HasFree TermAlpha Source #
Methods free :: TermAlpha -> Set Var Source # freeIn :: Var -> TermAlpha -> Bool Source # notFreeIn :: Var -> TermAlpha -> Bool Source # closed :: TermAlpha -> Bool Source #
HasFree Sequent Source #
Methods free :: Sequent -> Set Var Source # freeIn :: Var -> Sequent -> Bool Source # notFreeIn :: Var -> Sequent -> Bool Source # closed :: Sequent -> Bool Source #
HasFree Thm Source #
Methods free :: Thm -> Set Var Source # freeIn :: Var -> Thm -> Bool Source # notFreeIn :: Var -> Thm -> Bool Source # closed :: Thm -> Bool Source #
HasFree a => HasFree [a] Source #
Methods free :: [a] -> Set Var Source # freeIn :: Var -> [a] -> Bool Source # notFreeIn :: Var -> [a] -> Bool Source # closed :: [a] -> Bool Source #
HasFree a => HasFree (Set a) Source #
Methods free :: Set a -> Set Var Source # freeIn :: Var -> Set a -> Bool Source # notFreeIn :: Var -> Set a -> Bool Source # closed :: Set a -> Bool Source #

renameAvoiding :: Set Name -> Var -> Var Source #