Copyright | (c) 2014, Aleksey Kliger |
---|---|

License | BSD3 (See LICENSE) |

Maintainer | Aleksey Kliger |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

Extensions | DeriveGeneric |

# Documentation

If `p`

is a pattern type, then `Rec p`

is also a pattern type,
which is *recursive* in the sense that `p`

may bind names in terms
embedded within itself. Useful for encoding e.g. lectrec and
Agda's dot notation.

`TRec`

is a standalone variant of `Rec`

: the only difference is
that whereas

is a pattern type, `Rec`

p`TRec p`

is a *term type*. It is isomorphic to

.`Bind`

(`Rec`

p) ()

Note that `TRec`

corresponds to Pottier's *abstraction* construct
from alpha-Caml. In this context,

corresponds to
alpha-Caml's `Embed`

t`inner t`

, and

corresponds to
alpha-Caml's `Shift`

(`Embed`

t)`outer t`

.