Copyright	(c) 2014 Aleksey Kliger
License	BSD3 (See LICENSE)
Maintainer	Aleksey Kliger
Stability	experimental
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	DeriveGeneric

Unbound.Generics.LocallyNameless.Bind

Contents

Name binding

Description

The fundamental binding form. The type Bind p t allows you to place a pattern p in a term t such that the names in the pattern scope over the term. Use bind and unbind and lunbind to work with Bind p t

Synopsis

data Bind p t = B p t

Name binding

data Bind p t Source #

A term of type Bind p t is a term that binds the free variable occurrences of the variables in pattern p in the term t. In the overall term, those variables are now bound. See also bind and unbind and lunbind

Constructors

B p t

Instances

Instances details

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Subst Methods isvar :: Bind a b -> Maybe (SubstName (Bind a b) c) Source # isCoerceVar :: Bind a b -> Maybe (SubstCoerce (Bind a b) c) Source # subst :: Name c -> c -> Bind a b -> Bind a b Source # substs :: [(Name c, c)] -> Bind a b -> Bind a b Source # substBvs :: AlphaCtx -> [c] -> Bind a b -> Bind a b Source #
Generic (Bind p t) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Bind Associated Types type Rep (Bind p t) :: Type -> Type # Methods from :: Bind p t -> Rep (Bind p t) x # to :: Rep (Bind p t) x -> Bind p t #
(Show p, Show t) => Show (Bind p t) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Bind Methods showsPrec :: Int -> Bind p t -> ShowS # show :: Bind p t -> String # showList :: [Bind p t] -> ShowS #
(NFData p, NFData t) => NFData (Bind p t) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Bind Methods rnf :: Bind p t -> () #
(Alpha p, Alpha t) => Alpha (Bind p t) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Bind Methods aeq' :: AlphaCtx -> Bind p t -> Bind p t -> Bool Source # fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Bind p t -> f (Bind p t) Source # close :: AlphaCtx -> NamePatFind -> Bind p t -> Bind p t Source # open :: AlphaCtx -> NthPatFind -> Bind p t -> Bind p t Source # isPat :: Bind p t -> DisjointSet AnyName Source # isTerm :: Bind p t -> All Source # isEmbed :: Bind p t -> Bool Source # nthPatFind :: Bind p t -> NthPatFind Source # namePatFind :: Bind p t -> NamePatFind Source # swaps' :: AlphaCtx -> Perm AnyName -> Bind p t -> Bind p t Source # lfreshen' :: LFresh m => AlphaCtx -> Bind p t -> (Bind p t -> Perm AnyName -> m b) -> m b Source # freshen' :: Fresh m => AlphaCtx -> Bind p t -> m (Bind p t, Perm AnyName) Source # acompare' :: AlphaCtx -> Bind p t -> Bind p t -> Ordering Source #
type Rep (Bind p t) Source #
Instance details Defined in Unbound.Generics.LocallyNameless.Bind type Rep (Bind p t) = D1 ('MetaData "Bind" "Unbound.Generics.LocallyNameless.Bind" "unbound-generics-0.4.3-inplace" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))