bound-1.0.6: Making de Bruijn Succ Less

Copyright(C) 2012 Edward Kmett
LicenseBSD-style (see the file LICENSE)
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell98

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]