Copyright | (c) 2024 Yamada Ryo |
---|---|
License | MPL-2.0 (see the file LICENSE) |
Maintainer | ymdfield@outlook.jp |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | GHC2021 |
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
WeakenUnder_ 'True 0 'True 0 es es Source # | |
Defined in Data.Hefty.Union.Weaken | |
(Weaken (n - 1) es es', (n == 0) ~ 'False) => WeakenUnder_ 'True 0 'False n es (e ': es') Source # | |
Defined in Data.Hefty.Union.Weaken | |
(WeakenUnder n (m - 1) es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) => WeakenUnder_ 'False m isNZero n (e ': es) (e ': es') Source # | |
Defined in Data.Hefty.Union.Weaken |
type WeakenUnder n m = WeakenUnder_ (m == 0) m (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 #