Safe Haskell | Safe |
---|

# A Module for Lambda-Terms.

# Documentation

Lambda terms: variables, application, abstraction.

The set of all variables occurring in a term. For example

vars (App (Var "x") (Abs "y" (Var "y"))) == ["x", "y"]

The set of free variables occurring in a term. For example

fvs (App (Var "x") (Abs "y" (Var "y"))) == ["x"]

freshName :: Id -> [Id] -> (Id, Term -> Term) Source #

Given a variable `x`

and a set of variable names to avoid `ys`

, `freshName x ys`

computes a pair `(x', ren)`

such that `x'`

is a variable that is fresh for `ys`

(that is, different from all elements of `ys`

) and `ren :: Term -> Term`

is a
function that renames all occurrences of `x`

in a term by `x'`

.