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.

Constructors

B p t

Instances

(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)

data Rebind p1 p2 Source

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

Constructors

R p1 p2

Instances

(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)

data Rec p Source

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).

Constructors

Rec p

Instances

(Rep p[a1f6Y], Sat (ctx[a1fbd] p[a1f6Y])) => Rep1 ctx[a1fbd] (Rec p[a1f6Y])
(Alpha a, Subst c a) => Subst c (Rec a)
Show a => Show (Rec a)
Rep p[a1f6Y] => Rep (Rec p[a1f6Y])
Alpha p => Alpha (Rec p)

newtype TRec p Source

TRec is a standalone variant of Rec -- that is, if p is a pattern type then TRec p is a term type. It is isomorphic to Bind (Rec p) ().

Constructors

TRec (Bind (Rec p) ())

Instances

Show a => Show (TRec a)

newtype Embed t Source

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.

Constructors

Embed t

Instances

(Rep t[a1f6W], Sat (ctx[a1fby] t[a1f6W])) => Rep1 ctx[a1fby] (Embed t[a1f6W])
Subst c a => Subst c (Embed a)
Eq t => Eq (Embed t)
Show a => Show (Embed a)
Rep t[a1f6W] => Rep (Embed t[a1f6W])
Alpha t => Alpha (Embed t)

newtype Shift p Source

Shift the scope of an embedded term one level outwards.

Constructors

Shift p

Instances

(Rep p[a1f6V], Sat (ctx[a1fb5] p[a1f6V])) => Rep1 ctx[a1fb5] (Shift p[a1f6V])
Eq p => Eq (Shift p)
Show a => Show (Shift a)
Rep p[a1f6V] => Rep (Shift p[a1f6V])
Alpha a => Alpha (Shift a)

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.

rBind :: forall p[a1f71] t[a1f72]. (Rep p[a1f71], Rep t[a1f72]) => R (Bind p[a1f71] t[a1f72])Source

rRebind :: forall p1[a1f6Z] p2[a1f70]. (Rep p1[a1f6Z], Rep p2[a1f70]) => R (Rebind p1[a1f6Z] p2[a1f70])Source

rEmbed :: forall t[a1f6W]. Rep t[a1f6W] => R (Embed t[a1f6W])Source

rRec :: forall p[a1f6Y]. Rep p[a1f6Y] => R (Rec p[a1f6Y])Source

rShift :: forall p[a1f6V]. Rep p[a1f6V] => R (Shift p[a1f6V])Source