bound-0.8: Making de Bruijn Succ Less

Portabilityportable
Stabilityexperimental
MaintainerEdward Kmett <ekmett@gmail.com>
Safe HaskellSafe-Inferred

Bound.Term

Description

 

Synopsis

Documentation

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

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 aSource

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 -> BoolSource

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]