ideas-1.3.1: Feedback services for intelligent tutoring systems
Portabilityportable (depends on ghc)
Safe HaskellNone



Substitutions on terms. Substitutions are idempotent, and non-cyclic.



data Substitution Source

Abstract data type for substitutions

emptySubst :: Substitution Source

Returns the empty substitution

singletonSubst :: Int -> Term -> Substitution Source

Returns a singleton substitution

dom :: Substitution -> IntSet Source

Returns the domain of a substitution (as a set)

lookupVar :: Int -> Substitution -> Maybe Term Source

Lookups a variable in a substitution. Nothing indicates that the variable is not in the domain of the substitution

(@@) :: Substitution -> Substitution -> Substitution infixr 6 Source

Combines two substitutions. The left-hand side substitution is first applied to the co-domain of the right-hand side substitution

(|->) :: Substitution -> Term -> Term infixr 5 Source

Apply the substitution

listToSubst :: [(Int, Term)] -> Substitution Source

Turns a list into a substitution