Unbound.Generics.LocallyNameless.Bind

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

Name binding

data Bind p t

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

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Bind a b -> Maybe (SubstName (Bind a b) c)

isCoerceVar :: Bind a b -> Maybe (SubstCoerce (Bind a b) c)

subst :: Name c -> c -> Bind a b -> Bind a b

substs :: [(Name c, c)] -> Bind a b -> Bind a b

substBvs :: AlphaCtx -> [c] -> Bind a b -> Bind a b

Generic (Bind p t)

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)

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)

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

rnf :: Bind p t -> ()

(Alpha p, Alpha t) => Alpha (Bind p t)

Defined in Unbound.Generics.LocallyNameless.Bind

Methods

aeq' :: AlphaCtx -> Bind p t -> Bind p t -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Bind p t -> f (Bind p t)

close :: AlphaCtx -> NamePatFind -> Bind p t -> Bind p t

open :: AlphaCtx -> NthPatFind -> Bind p t -> Bind p t

isPat :: Bind p t -> DisjointSet AnyName

isTerm :: Bind p t -> All

isEmbed :: Bind p t -> Bool

nthPatFind :: Bind p t -> NthPatFind

namePatFind :: Bind p t -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Bind p t -> Bind p t

lfreshen' :: LFresh m => AlphaCtx -> Bind p t -> (Bind p t -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Bind p t -> m (Bind p t, Perm AnyName)

acompare' :: AlphaCtx -> Bind p t -> Bind p t -> Ordering

type Rep (Bind p t)

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