Safe Haskell	None
Language	Haskell2010

UVMHS.Lib.Substitution.SubstSpaced

Documentation

data SubstSpaced sG sS e Source #

Constructors

SubstSpaced
Fields substSpacedUnscoped :: sG ⇰ SubstElem sS e substSpacedScoped :: sS ⇰ SubstScoped sS e

Instances

Instances details

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

substSpacedUnscopedL :: SubstSpaced sG sS e ⟢ (sG ⇰ SubstElem sS e) Source #

substSpacedScopedL :: SubstSpaced sG sS e ⟢ (sS ⇰ SubstScoped sS e) Source #

isNullSubstSpaced :: Ord sS => SubstSpaced sG sS e -> 𝔹 Source #

wfSubstSpaced :: Ord sS => SubstSpaced sG sS e -> 𝔹 Source #

canonSubstSpaced :: (Ord sS, Eq e) => (sS -> e ⌲ DVar) -> ((sS ⇰ ℕ64) -> e -> 𝑂 e) -> (e -> e) -> SubstSpaced sG sS e -> SubstSpaced sG sS e Source #

shiftSubstSpaced :: Ord sS => (sS ⇰ ℕ64) -> SubstSpaced sG sS e -> SubstSpaced sG sS e Source #

introSubstSpaced :: (sS ⇰ ℕ64) -> SubstSpaced sG sS e Source #

sbindsSubstSpaced :: (sS ⇰ 𝕍 e) -> SubstSpaced sG sS e Source #

ubindsSubstSpaced :: (sG ⇰ e) -> SubstSpaced sG sS e Source #

substSpacedExtended :: (Ord sG, Ord sS) => (sS -> e ⌲ DVar) -> (SubstSpaced sG sS e -> e -> 𝑂 e) -> SubstSpaced sG sS e -> (sS ⇰ ℕ64) -> e -> 𝑂 e Source #

substSubstElemSpacedE :: (Ord sG, Ord sS) => (sS -> e ⌲ DVar) -> (SubstSpaced sG sS e -> e -> 𝑂 e) -> SubstSpaced sG sS e -> SubstElem sS e -> 𝑂 e Source #

substSubstElemSpaced :: (Ord sG, Ord sS) => (sS -> e ⌲ DVar) -> (SubstSpaced sG sS e -> e -> 𝑂 e) -> SubstSpaced sG sS e -> SubstElem sS e -> SubstElem sS e Source #

substSSubstElemSpaced :: (Ord sG, Ord sS) => (sS -> e ⌲ DVar) -> (SubstSpaced sG sS e -> e -> 𝑂 e) -> SubstSpaced sG sS e -> sS -> SSubstElem sS e -> SSubstElem sS e Source #

appendSubstSpaced :: (Ord sG, Ord sS) => (sS -> e ⌲ DVar) -> (SubstSpaced sG sS e -> e -> 𝑂 e) -> SubstSpaced sG sS e -> SubstSpaced sG sS e -> SubstSpaced sG sS e Source #