HOL.Subst

Documentation

data Subst

Constructors

Subst TypeSubst (Map Var Term) (Map Term (Maybe Term))

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

Minimal complete definition

basicSubst

Methods

basicSubst :: a -> Subst -> (Maybe a, Subst)

sharingSubst :: a -> Subst -> (Maybe a, Subst)

subst :: Subst -> a -> Maybe a

typeSubst :: TypeSubst -> a -> Maybe a

trySharingSubst :: a -> Subst -> (a, Subst)

trySubst :: Subst -> a -> a

tryTypeSubst :: TypeSubst -> a -> a

Instances

CanSubst Term

Methods

basicSubst :: Term -> Subst -> (Maybe Term, Subst)

sharingSubst :: Term -> Subst -> (Maybe Term, Subst)

subst :: Subst -> Term -> Maybe Term

typeSubst :: TypeSubst -> Term -> Maybe Term

trySharingSubst :: Term -> Subst -> (Term, Subst)

trySubst :: Subst -> Term -> Term

tryTypeSubst :: TypeSubst -> Term -> Term

CanSubst Var

Methods

basicSubst :: Var -> Subst -> (Maybe Var, Subst)

sharingSubst :: Var -> Subst -> (Maybe Var, Subst)

subst :: Subst -> Var -> Maybe Var

typeSubst :: TypeSubst -> Var -> Maybe Var

trySharingSubst :: Var -> Subst -> (Var, Subst)

trySubst :: Subst -> Var -> Var

tryTypeSubst :: TypeSubst -> Var -> Var

CanSubst Type

Methods

basicSubst :: Type -> Subst -> (Maybe Type, Subst)

sharingSubst :: Type -> Subst -> (Maybe Type, Subst)

subst :: Subst -> Type -> Maybe Type

typeSubst :: TypeSubst -> Type -> Maybe Type

trySharingSubst :: Type -> Subst -> (Type, Subst)

trySubst :: Subst -> Type -> Type

tryTypeSubst :: TypeSubst -> Type -> Type

CanSubst TermAlpha

Methods

basicSubst :: TermAlpha -> Subst -> (Maybe TermAlpha, Subst)

sharingSubst :: TermAlpha -> Subst -> (Maybe TermAlpha, Subst)

subst :: Subst -> TermAlpha -> Maybe TermAlpha

typeSubst :: TypeSubst -> TermAlpha -> Maybe TermAlpha

trySharingSubst :: TermAlpha -> Subst -> (TermAlpha, Subst)

trySubst :: Subst -> TermAlpha -> TermAlpha

tryTypeSubst :: TypeSubst -> TermAlpha -> TermAlpha

CanSubst Sequent

Methods

basicSubst :: Sequent -> Subst -> (Maybe Sequent, Subst)

sharingSubst :: Sequent -> Subst -> (Maybe Sequent, Subst)

subst :: Subst -> Sequent -> Maybe Sequent

typeSubst :: TypeSubst -> Sequent -> Maybe Sequent

trySharingSubst :: Sequent -> Subst -> (Sequent, Subst)

trySubst :: Subst -> Sequent -> Sequent

tryTypeSubst :: TypeSubst -> Sequent -> Sequent

CanSubst Thm

Methods

basicSubst :: Thm -> Subst -> (Maybe Thm, Subst)

sharingSubst :: Thm -> Subst -> (Maybe Thm, Subst)

subst :: Subst -> Thm -> Maybe Thm

typeSubst :: TypeSubst -> Thm -> Maybe Thm

trySharingSubst :: Thm -> Subst -> (Thm, Subst)

trySubst :: Subst -> Thm -> Thm

tryTypeSubst :: TypeSubst -> Thm -> Thm

CanSubst a => CanSubst [a]

Methods

basicSubst :: [a] -> Subst -> (Maybe [a], Subst)

sharingSubst :: [a] -> Subst -> (Maybe [a], Subst)

subst :: Subst -> [a] -> Maybe [a]

typeSubst :: TypeSubst -> [a] -> Maybe [a]

trySharingSubst :: [a] -> Subst -> ([a], Subst)

trySubst :: Subst -> [a] -> [a]

tryTypeSubst :: TypeSubst -> [a] -> [a]

(Ord a, CanSubst a) => CanSubst (Set a)

Methods

basicSubst :: Set a -> Subst -> (Maybe (Set a), Subst)

sharingSubst :: Set a -> Subst -> (Maybe (Set a), Subst)

subst :: Subst -> Set a -> Maybe (Set a)

typeSubst :: TypeSubst -> Set a -> Maybe (Set a)

trySharingSubst :: Set a -> Subst -> (Set a, Subst)

trySubst :: Subst -> Set a -> Set a

tryTypeSubst :: TypeSubst -> Set a -> Set a