Safe Haskell | None |
---|---|
Language | Haskell2010 |
- type Peano = Nat
- type family FromPeano (n :: Nat) :: Nat where ...
- type family ToPeano (n :: Nat) :: Nat where ...
- sFromPeano :: Sing n -> Sing (FromPeano n)
- sToPeano :: Sing n -> Sing (ToPeano n)
- fromPeanoInjective :: forall n m. (SingI n, SingI m) => (FromPeano n :=: FromPeano m) -> n :=: m
- toPeanoInjective :: (ToPeano n :=: ToPeano m) -> n :=: m
- fromToPeano :: Sing n -> FromPeano (ToPeano n) :=: n
- toFromPeano :: Sing n -> ToPeano (FromPeano n) :=: n
- fromPeanoZeroCong :: FromPeano Z :=: 0
- toPeanoZeroCong :: ToPeano 0 :=: Z
- fromPeanoOneCong :: FromPeano One :=: 1
- toPeanoOneCong :: ToPeano 1 :=: One
- fromPeanoSuccCong :: Sing n -> FromPeano (S n) :=: Succ (FromPeano n)
- toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :=: S (ToPeano n)
- fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n :+ m) :=: (FromPeano n + FromPeano m)
- toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n + m) :=: (ToPeano n :+ ToPeano m)
- fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n :* m) :=: (FromPeano n * FromPeano m)
- toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n :* m) :=: (ToPeano n :* ToPeano m)
- fromPeanoMonotone :: (n :<<= m) ~ True => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :=: True
- toPeanoMonotone :: n <= m => Sing n -> Sing m -> (ToPeano n :<<= ToPeano m) :~: True
- plusZR :: Sing n -> (n + 0) :~: n
- plusZL :: Sing n -> (0 + n) :~: n
- plusSuccR :: Sing n -> Sing m -> (n + Succ m) :~: Succ (n + m)
- plusSuccL :: Sing n -> Sing m -> (Succ n + m) :~: Succ (n + m)
- multZR :: Sing n -> (n * 0) :~: 0
- multZL :: Sing n -> (0 * n) :~: 0
- multSuccR :: Sing n -> Sing m -> (n * Succ m) :~: ((n * m) + n)
- multSuccL :: Sing n -> Sing m -> (Succ n * m) :~: ((n * m) + m)
- inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n
- plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n)
- multComm :: Sing n -> Sing m -> (n * m) :~: (m * n)
- plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))
- multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))
- plusMultDistr :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))
- multPlusDistr :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))
Sysnonym to avoid confusion
Coercion between builtin type-level natural and peano numerals
Properties of FromPeano
and ToPeano
.
FromPeano
ToPeano
fromPeanoInjective :: forall n m. (SingI n, SingI m) => (FromPeano n :=: FromPeano m) -> n :=: m Source #
Bijection
Algebraic isomorphisms
fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n :+ m) :=: (FromPeano n + FromPeano m) Source #
fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n :* m) :=: (FromPeano n * FromPeano m) Source #
fromPeanoMonotone :: (n :<<= m) ~ True => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :=: True Source #
Peano and commutative ring axioms for built-in Nat
Nat