TypeUnary.Nat

Contents

• Value-typed natural numbers
• Inequality proofs and indices

Description

Synopsis

• module TypeUnary.TyNat
• data Nat :: * -> * where
  • Zero :: Nat Z
  • Succ :: IsNat n => Nat n -> Nat (S n)
• predN :: Nat (S n) -> Nat n
• zero :: Nat N0
• one :: Nat N1
• two :: Nat N2
• three :: Nat N3
• four :: Nat N4
• withIsNat :: (IsNat n => Nat n -> a) -> Nat n -> a
• natSucc :: Nat n -> Nat (S n)
• natIsNat :: Nat n -> IsNat n => Nat n
• natToZ :: Num a => Nat n -> a
• natEq :: Nat m -> Nat n -> Maybe (m :=: n)
• natAdd :: Nat m -> Nat n -> Nat (m :+: n)
• natMul :: forall m n. Nat m -> Nat n -> Nat (m :*: n)
• class IsNat n where
• induction :: forall p. p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n))) -> forall n. IsNat n => Dict (p n)
• class (n :+: Z) ~ n => PlusZero n
• plusZero :: IsNat n => Dict (PlusZero n)
• data m :<: n where
  • ZLess :: Z :<: S n
  • SLess :: (m :<: n) -> S m :<: S n
• succLim :: (m :<: n) -> m :<: S n
• data Index lim = IsNat n => Index (n :<: lim) (Nat n)
• unIndex :: Num a => Index m -> a
• succI :: Index m -> Index (S m)
• index0 :: Index (N1 :+: m)
• index1 :: Index (N2 :+: m)
• index2 :: Index (N3 :+: m)
• index3 :: Index (N4 :+: m)
• coerceToIndex :: (Eq i, Show i, Num i, IsNat m) => i -> Index m

Documentation

Value-typed natural numbers

Inequality proofs and indices