Safe Haskell	None
Language	Haskell2010

UVMHS.Lib.Substitution.Subst

Documentation

newtype Subst s e Source #

Constructors

Subst
Fields unSubst :: SubstSpaced (s ∧ Name) (s ∧ SName) e

Instances

Instances details

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

unSubstL :: Subst s e ⟢ SubstSpaced (s ∧ Name) (s ∧ SName) e Source #

isNullSubst :: Ord s => Subst s e -> 𝔹 Source #

wfSubst :: Ord s => Subst s e -> 𝔹 Source #

canonSubstWith :: (Ord s, Eq e) => ((s ∧ SName) -> e ⌲ DVar) -> (((s ∧ SName) ⇰ ℕ64) -> e -> 𝑂 e) -> (e -> e) -> Subst s e -> Subst s e Source #

dshiftsSubst :: Ord s => (s ⇰ ℕ64) -> Subst s e -> Subst s e Source #

dshiftSubst :: Ord s => s -> ℕ64 -> Subst s e -> Subst s e Source #

dintrosSubst :: Ord s => (s ⇰ ℕ64) -> Subst s e Source #

dintroSubst :: Ord s => s -> ℕ64 -> Subst s e Source #

dbindsSubst :: Ord s => (s ⇰ 𝕍 e) -> Subst s e Source #

dbindSubst :: Ord s => s -> e -> Subst s e Source #

nshiftsSubst :: Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e -> Subst s e Source #

nshiftSubst :: Ord s => s -> Name -> ℕ64 -> Subst s e -> Subst s e Source #

nintrosSubst :: Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e Source #

nintroSubst :: Ord s => s -> Name -> ℕ64 -> Subst s e Source #

nbindsSubst :: Ord s => (s ⇰ (Name ⇰ 𝕍 e)) -> Subst s e Source #

nbindSubst :: Ord s => s -> Name -> e -> Subst s e Source #

gbindsSubst :: Ord s => (s ⇰ (Name ⇰ e)) -> Subst s e Source #

gbindSubst :: Ord s => s -> Name -> e -> Subst s e Source #

newtype MetaSubst s e Source #

Constructors

MetaSubst
Fields unMetaSubst :: (s ∧ Name) ⇰ SubstElem (s ∧ SName) e

Instances

Instances details

(Show s, Show e) => Show (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods showsPrec :: Int -> MetaSubst s e -> ShowS # show :: MetaSubst s e -> String # showList :: [MetaSubst s e] -> ShowS #
(Eq s, Eq e) => Eq (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods (==) :: MetaSubst s e -> MetaSubst s e -> Bool # (/=) :: MetaSubst s e -> MetaSubst s e -> Bool #
(Ord s, Ord e) => Ord (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods compare :: MetaSubst s e -> MetaSubst s e -> Ordering # (<) :: MetaSubst s e -> MetaSubst s e -> Bool # (<=) :: MetaSubst s e -> MetaSubst s e -> Bool # (>) :: MetaSubst s e -> MetaSubst s e -> Bool # (>=) :: MetaSubst s e -> MetaSubst s e -> Bool # max :: MetaSubst s e -> MetaSubst s e -> MetaSubst s e # min :: MetaSubst s e -> MetaSubst s e -> MetaSubst s e #
(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods fuzzy :: FuzzyM (MetaSubst s e) Source #
(Pretty s, Pretty e) => Pretty (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods pretty :: MetaSubst s e -> Doc Source #
(Ord s, Shrinky e) => Shrinky (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods shrink :: MetaSubst s e -> 𝐼 (MetaSubst s e) Source #

unMetaSubstL :: MetaSubst s e ⟢ ((s ∧ Name) ⇰ SubstElem (s ∧ SName) e) Source #

mbindsSubst :: Ord s => (s ⇰ (Name ⇰ e)) -> MetaSubst s e Source #

mbindSubst :: Ord s => s -> Name -> e -> MetaSubst s e Source #