Data.Hefty.Union.Strengthen

Documentation

class (Union u, isMZero ~ (m == 0), isNZero ~ (n == 0)) => StrengthenUnder_ (isMZero :: Bool) (m :: Natural) (isNZero :: Bool) (n :: Natural) u es es' | m n es -> es' where

Methods

strengthenNUnderM_ :: u es f ~> u es' f

Instances

Union u => StrengthenUnder_ 'True 0 'True 0 u es es

Defined in Data.Hefty.Union.Strengthen

Methods

strengthenNUnderM_ :: forall (f :: Type -> Type). u es f ~> u es f

(Union u, Strengthen (n - 1) u es es', MemberRec u e es, (n == 0) ~ 'False) => StrengthenUnder_ 'True 0 'False n u (e ': es) es'

Defined in Data.Hefty.Union.Strengthen

Methods

strengthenNUnderM_ :: forall (f :: Type -> Type). u (e ': es) f ~> u es' f

(Union u, StrengthenUnder n (m - 1) u es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) => StrengthenUnder_ 'False m isNZero n u (e ': es) (e ': es')

Defined in Data.Hefty.Union.Strengthen

Methods

strengthenNUnderM_ :: forall (f :: Type -> Type). u (e ': es) f ~> u (e ': es') f

type StrengthenUnder n m = StrengthenUnder_ (m == 0) m (n == 0) n

type Strengthen n = StrengthenUnder_ 'True 0 (n == 0) n

strengthenNUnderM :: forall n m u es' f es. StrengthenUnder n m u es es' => u es f ~> u es' f

strengthenN :: forall n u es' f es. Strengthen n u es es' => u es f ~> u es' f