bound-2.0.1: Making de Bruijn Succ Less

Bound.Term

Description

Synopsis

# Documentation

substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a Source #

substitute a p w replaces the free variable a with p in w.

>>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
["goodnight","Gracie","!!!"]


substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a Source #

substituteVar a b w replaces a free variable a with another free variable b in w.

>>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
["Bob","Bob","Charlie"]


isClosed :: Foldable f => f a -> Bool Source #

A closed term has no free variables.

>>> isClosed []
True

>>> isClosed [1,2,3]
False


closed :: Traversable f => f a -> Maybe (f b) Source #

If a term has no free variables, you can freely change the type of free variables it is parameterized on.

>>> closed [12]
Nothing

>>> closed ""
Just []

>>> :t closed ""
closed "" :: Maybe [b]