hol-1.4: Higher order logic
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

free

Methods

free :: a -> Set Var Source #

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

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

closed :: a -> Bool Source #

Instances

Instances details
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 #

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 #

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 #

HasFree TermAlpha Source # 
Instance details

Defined in HOL.TermAlpha

Methods

free :: TermAlpha -> Set Var Source #

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

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

closed :: TermAlpha -> Bool Source #

HasFree Sequent Source # 
Instance details

Defined in HOL.Sequent

Methods

free :: Sequent -> Set Var Source #

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

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

closed :: Sequent -> Bool Source #

HasFree Thm Source # 
Instance details

Defined in HOL.Thm

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 # 
Instance details

Defined in HOL.Var

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 # 
Instance details

Defined in HOL.Var

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 #