Stability | experimental |
---|---|
Maintainer | Aleksey Kliger |
Safe Haskell | None |
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
pTRec 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
tinner t
, and
corresponds to
alpha-Caml's Shift
(Embed
t)outer t
.