Safe Haskell	None
Language	Haskell2010

UVMHS.Lib.Substitution.SubstScoped

Documentation

data SubstScoped s e Source #

Constructors

SubstScoped

Fields

substScopedShift :: ℕ64
ρ: De Bruijn indices lower than this number will be untouched by this substitution. Think of it as a substitution working over all natural numbers being shifted to the right to ignore this many first indices.
substScopeElems :: 𝕍 (SSubstElem s e)
es: Instantiates as many of the first indices (post-shift by ρ) as the length of this vector with the values in the vector.
substScopeIntro :: ℤ64
ι: Starting at the nameless variable index after all the shifts (ρ) and all the instantiations (es), simulate an introduction of this many new nameless variables by bumping all subsequent indices by this much.

Instances

Instances details

(Lift s, Lift e) => Lift (SubstScoped s e :: Type) Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => SubstScoped s e -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => SubstScoped s e -> Code m (SubstScoped s e) #
Functor (SubstScoped s) Source #
Instance details Defined in UVMHS.Lib.Substitution.SubstScoped Methods map :: (a -> b) -> SubstScoped s a -> SubstScoped s b Source #
(Show s, Show e) => Show (SubstScoped s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.SubstScoped Methods showsPrec :: Int -> SubstScoped s e -> ShowS # show :: SubstScoped s e -> String # showList :: [SubstScoped s e] -> ShowS #
(Eq s, Eq e) => Eq (SubstScoped s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.SubstScoped Methods (==) :: SubstScoped s e -> SubstScoped s e -> Bool # (/=) :: SubstScoped s e -> SubstScoped s e -> Bool #
(Ord s, Ord e) => Ord (SubstScoped s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.SubstScoped Methods compare :: SubstScoped s e -> SubstScoped s e -> Ordering # (<) :: SubstScoped s e -> SubstScoped s e -> Bool # (<=) :: SubstScoped s e -> SubstScoped s e -> Bool # (>) :: SubstScoped s e -> SubstScoped s e -> Bool # (>=) :: SubstScoped s e -> SubstScoped s e -> Bool # max :: SubstScoped s e -> SubstScoped s e -> SubstScoped s e # min :: SubstScoped s e -> SubstScoped s e -> SubstScoped s e #
(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (SubstScoped s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.SubstScoped Methods fuzzy :: FuzzyM (SubstScoped s e) Source #
(Pretty e, Pretty s) => Pretty (SubstScoped s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.SubstScoped Methods pretty :: SubstScoped s e -> Doc Source #
(Ord s, Shrinky e) => Shrinky (SubstScoped s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.SubstScoped Methods shrink :: SubstScoped s e -> 𝐼 (SubstScoped s e) Source #

substScopedShiftL :: SubstScoped s e ⟢ ℕ64 Source #

substScopeElemsL :: SubstScoped s e ⟢ 𝕍 (SSubstElem s e) Source #

substScopeIntroL :: SubstScoped s e ⟢ ℤ64 Source #

lookupSubstScoped :: SubstScoped s e -> DVar -> SSubstElem s e Source #

interpSubstScoped :: (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstScoped s e -> DVar -> 𝑂 e Source #

wfSubstScoped :: SubstScoped s e -> 𝔹 Source #

canonSubstScoped :: (Eq s, Eq e) => (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> (e -> e) -> SubstScoped s e -> SubstScoped s e Source #

isNullSubstScoped :: SubstScoped s e -> 𝔹 Source #

introSubstScoped :: ℕ64 -> SubstScoped s e Source #

shiftSubstScoped :: Ord s => (s ⇰ ℕ64) -> s -> SubstScoped s e -> SubstScoped s e Source #

bindSubstScoped :: 𝕍 e -> SubstScoped s e Source #

substSubstScoped :: (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstScoped s e -> SubstScoped s e Source #

ppSubstScopedWith :: Pretty e => ((s ⇰ ℕ64) -> Doc) -> (DVarInf -> Doc) -> SubstScoped s e -> 𝐼 (Doc ∧ Doc) Source #