heftia-0.3.1.0: higher-order effects done right
Copyright(c) 2024 Yamada Ryo
LicenseMPL-2.0 (see the file LICENSE)
Maintainerymdfield@outlook.jp
Stabilityexperimental
Portabilityportable
Safe HaskellSafe-Inferred
LanguageGHC2021

Data.Hefty.Union.Weaken

Description

 

Documentation

class (isMZero ~ (m == 0), isNZero ~ (n == 0)) => WeakenUnder_ (isMZero :: Bool) (m :: Natural) (isNZero :: Bool) (n :: Natural) es es' | m n es' -> es where Source #

Methods

weakenNUnderM_ :: Union u => u es f ~> u es' f Source #

Instances

Instances details
WeakenUnder_ 'True 0 'True 0 es es Source # 
Instance details

Defined in Data.Hefty.Union.Weaken

Methods

weakenNUnderM_ :: forall (u :: [SigClass] -> SigClass) (f :: Type -> Type). Union u => u es f ~> u es f Source #

(Weaken (n - 1) es es', (n == 0) ~ 'False) => WeakenUnder_ 'True 0 'False n es (e ': es') Source # 
Instance details

Defined in Data.Hefty.Union.Weaken

Methods

weakenNUnderM_ :: forall (u :: [SigClass] -> SigClass) (f :: Type -> Type). Union u => u es f ~> u (e ': es') f Source #

(WeakenUnder n (m - 1) es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) => WeakenUnder_ 'False m isNZero n (e ': es) (e ': es') Source # 
Instance details

Defined in Data.Hefty.Union.Weaken

Methods

weakenNUnderM_ :: forall (u :: [SigClass] -> SigClass) (f :: Type -> Type). Union u => u (e ': es) f ~> u (e ': es') f Source #

type WeakenUnder n m = WeakenUnder_ (m == 0) m (n == 0) n Source #

type Weaken n = WeakenUnder_ 'True 0 (n == 0) n Source #

weakenNUnderM :: forall n m u es' f es. (Union u, WeakenUnder n m es es') => u es f ~> u es' f Source #

weakenN :: forall n u es' f es. (Union u, Weaken n es es') => u es f ~> u es' f Source #