Safe Haskell	None
Language	Haskell2010

UVMHS.Lib.Substitution.UVar

Documentation

data MVar s e Source #

Constructors

MVar
Fields mvarSubst :: Subst s e mvarName :: Name

Instances

Instances details

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

mvarSubstL :: MVar s e ⟢ Subst s e Source #

mvarNameL :: MVar s e ⟢ Name Source #

wfMVar :: Ord s => MVar s e -> 𝔹 Source #

data UVar s e Source #

Constructors

D_UVar DVar
N_UVar NVar
G_UVar GVar
M_UVar (MVar s e)

Instances

Instances details

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

d_UVarL :: UVar s e ⌲ DVar Source #

n_UVarL :: UVar s e ⌲ NVar Source #

g_UVarL :: UVar s e ⌲ GVar Source #

m_UVarL :: UVar s e ⌲ MVar s e Source #

name_UVarL :: UVar s e ⌲ Name Source #

uvar_Name :: Name -> UVar s e Source #

uvar_SVar :: SVar -> UVar s e Source #

svar_UVarL :: UVar s e ⌲ SVar Source #

uvar_Var :: Var -> UVar s e Source #

var_UVarL :: UVar s e ⌲ Var Source #

gensymUVar :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m (UVar s e) Source #

wfUVar :: Ord s => UVar s e -> 𝔹 Source #