Unbound.Generics.LocallyNameless

The purpose of unbound-genrics is to simplify the construction of data structures with rich variable binding structure by providing generic implementations of alpha-equivalence (aeq), free variable permutation (swaps), local and glocal variable freshness (lfresh, fresh),

See Alpha, Bind, Unbound.Generics.LocallyNameless.Operations for more information.

Documentation

module Unbound.Generics.LocallyNameless.Alpha

module Unbound.Generics.LocallyNameless.Name

module Unbound.Generics.LocallyNameless.Operations

module Unbound.Generics.LocallyNameless.Bind

module Unbound.Generics.LocallyNameless.Embed

module Unbound.Generics.LocallyNameless.Shift

module Unbound.Generics.LocallyNameless.Rebind

module Unbound.Generics.LocallyNameless.Rec

module Unbound.Generics.LocallyNameless.Fresh

module Unbound.Generics.LocallyNameless.LFresh

module Unbound.Generics.LocallyNameless.Subst