| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Strongweak.WeakenN.Internal
Description
WeakenN internals.
Just in case. You shouldn't need these, but they might be fun to look at.
Internal module. Exports may change without warning. Try not to use.
Synopsis
- class WeakenWeakenN (n :: Natural) a where
- weakenWeakenN :: a -> WeakenedN n a
- weakenedNRL1 :: forall (n :: Natural) a. WeakenedN (n - 1) (Weakened a) -> WeakenedN n a
- class WeakenWeakenN n a => StrengthenWeakenN (n :: Natural) a where
- strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a
- weakenedNLR1 :: forall (n :: Natural) a. WeakenedN n a -> WeakenedN (n - 1) (Weakened a)
Documentation
class WeakenWeakenN (n :: Natural) a where Source #
Methods
weakenWeakenN :: a -> WeakenedN n a Source #
Instances
| (Weaken a, WeakenWeakenN (n - 1) (Weakened a)) => WeakenWeakenN n a Source # | Inductive case. |
Defined in Strongweak.WeakenN.Internal Methods weakenWeakenN :: a -> WeakenedN n a Source # | |
| WeakenWeakenN 0 a Source # | Zero case: return the value as-is. |
Defined in Strongweak.WeakenN.Internal Methods weakenWeakenN :: a -> WeakenedN 0 a Source # | |
weakenedNRL1 :: forall (n :: Natural) a. WeakenedN (n - 1) (Weakened a) -> WeakenedN n a Source #
Inverted inductive WeakenedNcase.
n must not be 0.
class WeakenWeakenN n a => StrengthenWeakenN (n :: Natural) a where Source #
Methods
strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a Source #
Instances
| (Strengthen a, StrengthenWeakenN (n - 1) (Weakened a)) => StrengthenWeakenN n a Source # | |
Defined in Strongweak.WeakenN.Internal Methods strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a Source # | |
| StrengthenWeakenN 0 a Source # | |
Defined in Strongweak.WeakenN.Internal Methods strengthenWeakenN :: WeakenedN 0 a -> Either StrengthenFailure' a Source # | |