Unbound.Generics.LocallyNameless.Shift

The pattern Shift e shifts the scope of the embedded term in e one level outwards.

Documentation

newtype Shift e

The type Shift e is an embedding pattern that shifts the scope of the free variables of the embedded term Embedded e up by one level.

Constructors

Shift e

Instances

Functor Shift

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

fmap :: (a -> b) -> Shift a -> Shift b

(<$) :: a -> Shift b -> Shift a

Subst c e => Subst c (Shift e)

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Shift e -> Maybe (SubstName (Shift e) c)

isCoerceVar :: Shift e -> Maybe (SubstCoerce (Shift e) c)

subst :: Name c -> c -> Shift e -> Shift e

substs :: [(Name c, c)] -> Shift e -> Shift e

substBvs :: AlphaCtx -> [c] -> Shift e -> Shift e

Show e => Show (Shift e)

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

showsPrec :: Int -> Shift e -> ShowS

show :: Shift e -> String

showList :: [Shift e] -> ShowS

NFData e => NFData (Shift e)

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

rnf :: Shift e -> ()

Alpha e => Alpha (Shift e)

Defined in Unbound.Generics.LocallyNameless.Shift

Methods

aeq' :: AlphaCtx -> Shift e -> Shift e -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Shift e -> f (Shift e)

close :: AlphaCtx -> NamePatFind -> Shift e -> Shift e

open :: AlphaCtx -> NthPatFind -> Shift e -> Shift e

isPat :: Shift e -> DisjointSet AnyName

isTerm :: Shift e -> All

isEmbed :: Shift e -> Bool

nthPatFind :: Shift e -> NthPatFind

namePatFind :: Shift e -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Shift e -> Shift e

lfreshen' :: LFresh m => AlphaCtx -> Shift e -> (Shift e -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Shift e -> m (Shift e, Perm AnyName)

acompare' :: AlphaCtx -> Shift e -> Shift e -> Ordering

IsEmbed e => IsEmbed (Shift e)

Defined in Unbound.Generics.LocallyNameless.Shift

Associated Types

type Embedded (Shift e)

Methods

embedded :: (Profunctor p, Functor f) => p (Embedded (Shift e)) (f (Embedded (Shift e))) -> p (Shift e) (f (Shift e))

type Embedded (Shift e)

Defined in Unbound.Generics.LocallyNameless.Shift

type Embedded (Shift e) = Embedded e