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 :: forall n m. (KnownNat n, KnownNat m) => (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
- class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat) => IsPeano nat where
- inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n
- snat :: QuasiQuoter
- module Data.Singletons.Prelude.Eq
- module Data.Singletons.Prelude.Num
- module Data.Singletons.Prelude.Ord
- type (<) a b = (:<) a b
- type (<@#@$) = (:<$)
- type (<@#@$$) = (:<$$)
- type (<@#@$$$) a b = (:<$$$) a b
- (%<) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<) a b)
- type (>) a b = (:>) a b
- type (>@#@$) = (:>$)
- type (>@#@$$) = (:>$$)
- type (>@#@$$$) a b = (:>$$$) a b
- (%>) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>) a b)
- type (<=) a b = (:<=) a b
- type (<=@#@$) = (:<=$)
- type (<=@#@$$) = (:<=$$)
- type (<=@#@$$$) a b = (:<=$$$) a b
- (%<=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<=) a b)
- type (>=) a b = (:>=) a b
- type (>=@#@$) = (:>=$)
- type (>=@#@$$) = (:>=$$)
- type (>=@#@$$$) a b = (:>=$$$) a b
- (%>=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>=) a b)
- type (/=) a b = (:/=) a b
- type (/=@#@$) = (:/=$)
- type (/=@#@$$) = (:/=$$)
- type (/=@#@$$$) a b = (:/=$$$) a b
- (%/=) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((/=) a b)
- type (==) a b = (:==) a b
- type (==@#@$) = (:==$)
- type (==@#@$$) = (:==$$)
- type (==@#@$$$) a b = (:==$$$) a b
- (%==) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((==) a b)
- type (+) a b = (:+) a b
- type (+@#@$) = (:+$)
- type (+@#@$$) = (:+$$)
- type (+@#@$$$) a b = (:+$$$) a b
- (%+) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((+) a b)
- type (-) a b = (:-) a b
- type (-@#@$) = (:-$)
- type (-@#@$$) = (:-$$)
- type (-@#@$$$) a b = (:-$$$) a b
- (%-) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((-) a b)
- type * a b = (:*) a b
- type (*@#@$) = (:*$)
- type (*@#@$$) = (:*$$)
- type (*@#@$$$) a b = (:*$$$) a b
- (%*) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing (* a b)
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 #
toPeanoInjective :: forall n m. (KnownNat n, KnownNat m) => (ToPeano n :~: ToPeano m) -> n :~: m Source #
Bijection
Algebraic isomorphisms
fromPeanoMonotone :: (n <= m) ~ True => Sing n -> Sing m -> (FromPeano n <=? FromPeano m) :~: True Source #
Peano and commutative ring axioms for built-in Nat
Nat
class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat) => IsPeano nat where Source #
succOneCong, succNonCyclic, predSucc, plusMinus, succInj, (plusZeroL, plusSuccL | plusZeroR, plusZeroL), (multZeroL, multSuccL | multZeroR, multSuccR), induction
succOneCong :: Succ (Zero nat) :~: One nat Source #
succInj :: (Succ n :~: Succ (m :: nat)) -> n :~: m Source #
succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ (m :: nat)) -> n :~: m Source #
succNonCyclic :: Sing n -> (Succ n :~: Zero nat) -> Void Source #
induction :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k Source #
plusMinus :: Sing (n :: nat) -> Sing m -> ((n + m) - m) :~: n Source #
plusMinus' :: Sing (n :: nat) -> Sing m -> ((n + m) - n) :~: m Source #
plusZeroL :: Sing n -> (Zero nat + n) :~: n Source #
plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m :: nat) Source #
plusZeroR :: Sing n -> (n + Zero nat) :~: n Source #
plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m :: nat) Source #
plusComm :: Sing n -> Sing m -> (n + m) :~: ((m :: nat) + n) Source #
plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l)) Source #
multZeroL :: Sing n -> (Zero nat * n) :~: Zero nat Source #
multSuccL :: Sing (n :: nat) -> Sing m -> (S n * m) :~: ((n * m) + m) Source #
multZeroR :: Sing n -> (n * Zero nat) :~: Zero nat Source #
multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + (n :: nat)) Source #
multComm :: Sing (n :: nat) -> Sing m -> (n * m) :~: (m * n) Source #
multOneR :: Sing n -> (n * One nat) :~: n Source #
multOneL :: Sing n -> (One nat * n) :~: n Source #
plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l)) Source #
multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l)) Source #
minusNilpotent :: Sing n -> (n - n) :~: Zero nat Source #
multAssoc :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l)) Source #
plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l Source #
plusEqCancelR :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m Source #
succAndPlusOneL :: Sing n -> Succ n :~: (One nat + n) Source #
succAndPlusOneR :: Sing n -> Succ n :~: (n + One nat) Source #
predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat) Source #
zeroOrSucc :: Sing (n :: nat) -> ZeroOrSucc n Source #
plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> n :~: Zero nat Source #
plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> m :~: Zero nat Source #
predUnique :: Sing (n :: nat) -> Sing m -> (Succ n :~: m) -> n :~: Pred m Source #
multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n) Source #
multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m) Source #
minusZero :: Sing n -> (n - Zero nat) :~: n Source #
multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m Source #
succPred :: Sing n -> ((n :~: Zero nat) -> Void) -> Succ (Pred n) :~: n Source #
multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l Source #
sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat) Source #
toNatural :: Sing (n :: nat) -> Natural Source #
fromNatural :: Natural -> SomeSing nat Source #
inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n Source #
Induction scheme for built-in
.Nat
QuasiQuotes
snat :: QuasiQuoter Source #
Re-exports
module Data.Singletons.Prelude.Eq
module Data.Singletons.Prelude.Num
module Data.Singletons.Prelude.Ord
(%<) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<) a b) infix 4 Source #
(%>) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>) a b) infix 4 Source #
type (<=@#@$$$) a b = (:<=$$$) a b Source #
(%<=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<=) a b) infix 4 Source #
type (>=@#@$$$) a b = (:>=$$$) a b Source #
(%>=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>=) a b) infix 4 Source #
type (/=@#@$$$) a b = (:/=$$$) a b Source #
(%/=) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((/=) a b) infix 4 Source #
type (==@#@$$$) a b = (:==$$$) a b Source #
(%==) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((==) a b) infix 4 Source #
(%+) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((+) a b) infixl 6 Source #
(%-) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((-) a b) infixl 6 Source #
(%*) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing (* a b) infixl 7 Source #