Safe Haskell	None
Language	Haskell2010

UVMHS.Lib.Substitution.SubstElem

Documentation

data SubstElem s e Source #

Constructors

SubstElem
Fields substElemIntro :: s ⇰ ℕ64 delayed renaming , substElemValue ∷ () → 𝑂 e -- ^ delayed element substelemValue :: 𝑂 e

Instances

Instances details

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

substElemIntroL :: SubstElem s e ⟢ (s ⇰ ℕ64) Source #

substelemValueL :: SubstElem s e ⟢ 𝑂 e Source #

interpSubstElem :: ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e Source #

canonSubstElem :: ((s ⇰ ℕ64) -> e -> 𝑂 e) -> (e -> e) -> SubstElem s e -> SubstElem s e Source #

eqSubstElem :: Eq e => ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e -> 𝔹 Source #

compareSubstElem :: Ord e => ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e -> Ordering Source #

introSubstElem :: Ord s => (s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e Source #

substSubstElemE :: ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e Source #

substSubstElem :: ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e Source #

ppSubstElemNamed :: Pretty e => ((s ⇰ ℕ64) -> Doc) -> SubstElem s e -> Doc Source #

data SSubstElem s e Source #

Constructors

Var_SSE DVar
Trm_SSE (SubstElem s e)

Instances

Instances details

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

mkSSubstElem :: (e ⌲ DVar) -> 𝑂 e -> SSubstElem s e Source #

interpSSubstElem :: (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> 𝑂 e Source #

canonSSubstElem :: (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> (e -> e) -> SSubstElem s e -> SSubstElem s e Source #

eqSSubstElem :: Eq e => (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e -> 𝔹 Source #

compareSSubstElem :: Ord e => (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e -> Ordering Source #

introSSubstElem :: Ord s => s -> (s ⇰ ℕ64) -> SSubstElem s e -> SSubstElem s e Source #

substSSubstElem :: (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e Source #

ppSSubstElemNamed :: Pretty e => ((s ⇰ ℕ64) -> Doc) -> (DVarInf -> Doc) -> SSubstElem s e -> Doc Source #