- data Bind p t = B p t
- data Rebind p1 p2 = R p1 p2
- data Rec p = Rec p
- newtype TRec p = TRec (Bind (Rec p) ())
- newtype Embed t = Embed t
- newtype Shift p = Shift p
- module Unbound.LocallyNameless.Name
- rBind :: forall p[a1f71] t[a1f72]. (Rep p[a1f71], Rep t[a1f72]) => R (Bind p[a1f71] t[a1f72])
- rRebind :: forall p1[a1f6Z] p2[a1f70]. (Rep p1[a1f6Z], Rep p2[a1f70]) => R (Rebind p1[a1f6Z] p2[a1f70])
- rEmbed :: forall t[a1f6W]. Rep t[a1f6W] => R (Embed t[a1f6W])
- rRec :: forall p[a1f6Y]. Rep p[a1f6Y] => R (Rec p[a1f6Y])
- rShift :: forall p[a1f6V]. Rep p[a1f6V] => R (Shift p[a1f6V])

# Documentation

The type of a binding. We can `Bind`

an `a`

object in a `b`

object if we can create "fresh" `a`

objects, and `a`

objects
can occur unbound in `b`

objects. Often `a`

is `Name`

but that
need not be the case.

Like `Name`

, `Bind`

is also abstract. You can create bindings
using `bind`

and take them apart with `unbind`

and friends.

B p t |

(Rep p[a1f71], Rep t[a1f72], Sat (ctx[a1fbG] p[a1f71]), Sat (ctx[a1fbG] t[a1f72])) => Rep1 ctx[a1fbG] (Bind p[a1f71] t[a1f72]) | |

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) | |

(Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) | |

(Show a, Show b) => Show (Bind a b) | |

(Rep p[a1f71], Rep t[a1f72]) => Rep (Bind p[a1f71] t[a1f72]) | |

(Alpha p, Alpha t) => Alpha (Bind p t) |

`Rebind`

supports "telescopes" --- that is, patterns where
bound variables appear in multiple subterms.

R p1 p2 |

(Rep p1[a1f6Z], Rep p2[a1f70], Sat (ctx[a1fbl] p1[a1f6Z]), Sat (ctx[a1fbl] p2[a1f70])) => Rep1 ctx[a1fbl] (Rebind p1[a1f6Z] p2[a1f70]) | |

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Rebind a b) | |

(Alpha a, Alpha b, Eq b) => Eq (Rebind a b) | Compare for alpha-equality. |

(Show a, Show b) => Show (Rebind a b) | |

(Rep p1[a1f6Z], Rep p2[a1f70]) => Rep (Rebind p1[a1f6Z] p2[a1f70]) | |

(Alpha p, Alpha q) => Alpha (Rebind p q) |

`Rec`

supports recursive patterns --- that is, patterns where
any variables anywhere in the pattern are bound in the pattern
itself. Useful for lectrec (and Agda's dot notation).

Rec p |

An annotation is a "hole" in a pattern where variables can be used, but not bound. For example, patterns may include type annotations, and those annotations can reference variables without binding them. Annotations do nothing special when they appear elsewhere in terms.

Embed t |

Shift the scope of an embedded term one level outwards.

Shift p |

module Unbound.LocallyNameless.Name

# Pay no attention to the man behind the curtain

These type representation objects are exported so they can be referenced by auto-generated code. Please pretend they do not exist.