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.
Rec p |
Instances
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
.
Instances
(Alpha p, Subst c p) => Subst c (TRec p) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Subst | |||||
Generic (TRec p) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Rec
| |||||
Show a => Show (TRec a) Source # | |||||
Alpha p => Alpha (TRec p) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Rec aeq' :: AlphaCtx -> TRec p -> TRec p -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> TRec p -> f (TRec p) Source # close :: AlphaCtx -> NamePatFind -> TRec p -> TRec p Source # open :: AlphaCtx -> NthPatFind -> TRec p -> TRec p Source # isPat :: TRec p -> DisjointSet AnyName Source # isTerm :: TRec p -> All Source # isEmbed :: TRec p -> Bool Source # nthPatFind :: TRec p -> NthPatFind Source # namePatFind :: TRec p -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> TRec p -> TRec p Source # lfreshen' :: LFresh m => AlphaCtx -> TRec p -> (TRec p -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> TRec p -> m (TRec p, Perm AnyName) Source # acompare' :: AlphaCtx -> TRec p -> TRec p -> Ordering Source # | |||||
type Rep (TRec p) Source # | |||||
Defined in Unbound.Generics.LocallyNameless.Rec |