Data.Type.Natural.Builtin

Coercion between Peano Numerals Nat and builtin naturals Nat

Sysnonym to avoid confusion

type Peano = Nat

Type synonym for Nat to avoid confusion with built-in Nat.

Coercion between builtin type-level natural and peano numerals

type family FromPeano (n :: Nat) :: Nat where ...

Equations

FromPeano Z = 0

FromPeano (S n) = Succ (FromPeano n)

type family ToPeano (n :: Nat) :: Nat where ...

Equations

ToPeano 0 = Z

ToPeano n = S (ToPeano (Pred n))

sFromPeano :: Sing n -> Sing (FromPeano n)

sToPeano :: Sing n -> Sing (ToPeano n)

Properties of FromPeano and ToPeano.

fromPeanoInjective :: forall n m. (SingI n, SingI m) => (FromPeano n :~: FromPeano m) -> n :~: m

toPeanoInjective :: (ToPeano n :~: ToPeano m) -> n :~: m

Bijection

fromToPeano :: Sing n -> FromPeano (ToPeano n) :~: n

toFromPeano :: Sing n -> ToPeano (FromPeano n) :~: n

Algebraic isomorphisms

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

Peano and commutative ring axioms for built-in Nat

class (SDecide nat, SNum nat, SEnum nat) => IsPeano nat where

Minimal complete definition

succOneCong, succNonCyclic, predSucc, plusMinus, succInj, (plusZeroL, plusSuccL | plusZeroR, plusZeroL), (multZeroL, multSuccL | multZeroR, multSuccR), induction

Methods

succOneCong :: Succ (Zero nat) :~: One nat

succInj :: (Succ n :~: Succ (m :: nat)) -> n :~: m

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ (m :: nat)) -> n :~: m

succNonCyclic :: Sing n -> (Succ n :~: Zero nat) -> Void

induction :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k

plusMinus :: Sing (n :: nat) -> Sing m -> ((n :+ m) :- m) :~: n

plusMinus' :: Sing (n :: nat) -> Sing m -> ((n :+ m) :- n) :~: m

plusZeroL :: Sing n -> (Zero nat :+ n) :~: n

plusSuccL :: Sing n -> Sing m -> (S n :+ m) :~: S (n :+ m :: nat)

plusZeroR :: Sing n -> (n :+ Zero nat) :~: n

plusSuccR :: Sing n -> Sing m -> (n :+ S m) :~: S (n :+ m :: nat)

plusComm :: Sing n -> Sing m -> (n :+ m) :~: ((m :: nat) :+ n)

plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n :+ m) :+ l) :~: (n :+ (m :+ l))

multZeroL :: Sing n -> (Zero nat :* n) :~: Zero nat

multSuccL :: Sing (n :: nat) -> Sing m -> (S n :* m) :~: ((n :* m) :+ m)

multZeroR :: Sing n -> (n :* Zero nat) :~: Zero nat

multSuccR :: Sing n -> Sing m -> (n :* S m) :~: ((n :* m) :+ (n :: nat))

multComm :: Sing (n :: nat) -> Sing m -> (n :* m) :~: (m :* n)

multOneR :: Sing n -> (n :* One nat) :~: n

multOneL :: Sing n -> (One nat :* n) :~: n

plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> ((n :+ m) :* l) :~: ((n :* l) :+ (m :* l))

multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> (n :* (m :+ l)) :~: ((n :* m) :+ (n :* l))

minusNilpotent :: Sing n -> (n :- n) :~: Zero nat

multAssoc :: Sing (n :: nat) -> Sing m -> Sing l -> ((n :* m) :* l) :~: (n :* (m :* l))

plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n :+ m) :~: (n :+ l)) -> m :~: l

plusEqCancelR :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n :+ l) :~: (m :+ l)) -> n :~: m

succAndPlusOneL :: Sing n -> Succ n :~: (One nat :+ n)

succAndPlusOneR :: Sing n -> Succ n :~: (n :+ One nat)

predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat)

zeroOrSucc :: Sing (n :: nat) -> ZeroOrSucc n

plusEqZeroL :: Sing n -> Sing m -> ((n :+ m) :~: Zero nat) -> n :~: Zero nat

plusEqZeroR :: Sing n -> Sing m -> ((n :+ m) :~: Zero nat) -> m :~: Zero nat

predUnique :: Sing (n :: nat) -> Sing m -> (Succ n :~: m) -> n :~: Pred m

multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n :* m) :~: Succ l) -> n :~: Succ (Pred n)

multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n :* m) :~: Succ l) -> m :~: Succ (Pred m)

minusZero :: Sing n -> (n :- Zero nat) :~: n

multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n :* Succ l) :~: (m :* Succ l)) -> n :~: m

succPred :: Sing n -> ((n :~: Zero nat) -> Void) -> Succ (Pred n) :~: n

multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((Succ n :* m) :~: (Succ n :* l)) -> m :~: l

sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)

inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n

Induction scheme for built-in Nat.

QuasiQuotes

snat :: QuasiQuoter

Quotesi-quoter for singleton types for Nat. This can be used for an expression.

For example: [snat|12|] %:+ [snat| 5 |].

Orphan instances

IsPeano Nat

Methods

succOneCong :: (Nat :~: Succ Nat (Zero Nat)) (One Nat)

succInj :: (Nat :~: Succ Nat n) (Succ Nat m) -> (Nat :~: n) m

succInj' :: proxy n -> proxy' m -> (Nat :~: Succ Nat n) (Succ Nat m) -> (Nat :~: n) m

succNonCyclic :: Sing Nat n -> (Nat :~: Succ Nat n) (Zero Nat) -> Void

induction :: p (Zero Nat) -> (forall n. Sing Nat n -> p n -> p (S Nat n)) -> Sing Nat k -> p k

plusMinus :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :- (Nat :+ n) m) m) n

plusMinus' :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :- (Nat :+ n) m) n) m

plusZeroL :: Sing Nat n -> (Nat :~: (Nat :+ Zero Nat) n) n

plusSuccL :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :+ S Nat n) m) (S Nat ((Nat :+ n) m))

plusZeroR :: Sing Nat n -> (Nat :~: (Nat :+ n) (Zero Nat)) n

plusSuccR :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :+ n) (S Nat m)) (S Nat ((Nat :+ n) m))

plusComm :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :+ n) m) ((Nat :+ m) n)

plusAssoc :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :+ (Nat :+ n) m) l) ((Nat :+ n) ((Nat :+ m) l))

multZeroL :: Sing Nat n -> (Nat :~: (Nat :* Zero Nat) n) (Zero Nat)

multSuccL :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :* S Nat n) m) ((Nat :+ (Nat :* n) m) m)

multZeroR :: Sing Nat n -> (Nat :~: (Nat :* n) (Zero Nat)) (Zero Nat)

multSuccR :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :* n) (S Nat m)) ((Nat :+ (Nat :* n) m) n)

multComm :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :* n) m) ((Nat :* m) n)

multOneR :: Sing Nat n -> (Nat :~: (Nat :* n) (One Nat)) n

multOneL :: Sing Nat n -> (Nat :~: (Nat :* One Nat) n) n

plusMultDistrib :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :* (Nat :+ n) m) l) ((Nat :+ (Nat :* n) l) ((Nat :* m) l))

multPlusDistrib :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :* n) ((Nat :+ m) l)) ((Nat :+ (Nat :* n) m) ((Nat :* n) l))

minusNilpotent :: Sing Nat n -> (Nat :~: (Nat :- n) n) (Zero Nat)

multAssoc :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :* (Nat :* n) m) l) ((Nat :* n) ((Nat :* m) l))

plusEqCancelL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :+ n) m) ((Nat :+ n) l) -> (Nat :~: m) l

plusEqCancelR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :+ n) l) ((Nat :+ m) l) -> (Nat :~: n) m

succAndPlusOneL :: Sing Nat n -> (Nat :~: Succ Nat n) ((Nat :+ One Nat) n)

succAndPlusOneR :: Sing Nat n -> (Nat :~: Succ Nat n) ((Nat :+ n) (One Nat))

predSucc :: Sing Nat n -> (Nat :~: Pred Nat (Succ Nat n)) n

zeroOrSucc :: Sing Nat n -> ZeroOrSucc Nat n

plusEqZeroL :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :+ n) m) (Zero Nat) -> (Nat :~: n) (Zero Nat)

plusEqZeroR :: Sing Nat n -> Sing Nat m -> (Nat :~: (Nat :+ n) m) (Zero Nat) -> (Nat :~: m) (Zero Nat)

predUnique :: Sing Nat n -> Sing Nat m -> (Nat :~: Succ Nat n) m -> (Nat :~: n) (Pred Nat m)

multEqSuccElimL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :* n) m) (Succ Nat l) -> (Nat :~: n) (Succ Nat (Pred Nat n))

multEqSuccElimR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :* n) m) (Succ Nat l) -> (Nat :~: m) (Succ Nat (Pred Nat m))

minusZero :: Sing Nat n -> (Nat :~: (Nat :- n) (Zero Nat)) n

multEqCancelR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :* n) (Succ Nat l)) ((Nat :* m) (Succ Nat l)) -> (Nat :~: n) m

succPred :: Sing Nat n -> ((Nat :~: n) (Zero Nat) -> Void) -> (Nat :~: Succ Nat (Pred Nat n)) n

multEqCancelL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :* Succ Nat n) m) ((Nat :* Succ Nat n) l) -> (Nat :~: m) l

sPred' :: proxy n -> Sing Nat (Succ Nat n) -> Sing Nat n

PeanoOrder Nat

Methods

leqToCmp :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat :<= a) b) -> Either ((Nat :~: a) b) ((Ordering :~: Compare Nat a b) LT)

eqlCmpEQ :: Sing Nat a -> Sing Nat b -> (Nat :~: a) b -> (Ordering :~: Compare Nat a b) EQ

eqToRefl :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) EQ -> (Nat :~: a) b

flipCompare :: Sing Nat a -> Sing Nat b -> (Ordering :~: FlipOrdering (Compare Nat a b)) (Compare Nat b a)

ltToNeq :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) LT -> (Nat :~: a) b -> Void

leqNeqToLT :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat :<= a) b) -> ((Nat :~: a) b -> Void) -> (Ordering :~: Compare Nat a b) LT

succLeqToLT :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat :<= S Nat a) b) -> (Ordering :~: Compare Nat a b) LT

ltToLeq :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) LT -> IsTrue ((Nat :<= a) b)

gtToLeq :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) GT -> IsTrue ((Nat :<= b) a)

ltToSuccLeq :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) LT -> IsTrue ((Nat :<= Succ Nat a) b)

cmpZero :: Sing Nat a -> (Ordering :~: Compare Nat (Zero Nat) (Succ Nat a)) LT

leqToGT :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat :<= Succ Nat b) a) -> (Ordering :~: Compare Nat a b) GT

cmpZero' :: Sing Nat a -> Either ((Ordering :~: Compare Nat (Zero Nat) a) EQ) ((Ordering :~: Compare Nat (Zero Nat) a) LT)

zeroNoLT :: Sing Nat a -> (Ordering :~: Compare Nat a (Zero Nat)) LT -> Void

ltRightPredSucc :: Sing Nat a -> Sing Nat b -> (Ordering :~: Compare Nat a b) LT -> (Nat :~: b) (Succ Nat (Pred Nat b))

cmpSucc :: Sing Nat n -> Sing Nat m -> (Ordering :~: Compare Nat n m) (Compare Nat (Succ Nat n) (Succ Nat m))

ltSucc :: Sing Nat a -> (Ordering :~: Compare Nat a (Succ Nat a)) LT

cmpSuccStepR :: Sing Nat n -> Sing Nat m -> (Ordering :~: Compare Nat n m) LT -> (Ordering :~: Compare Nat n (Succ Nat m)) LT

ltSuccLToLT :: Sing Nat n -> Sing Nat m -> (Ordering :~: Compare Nat (Succ Nat n) m) LT -> (Ordering :~: Compare Nat n m) LT

leqToLT :: Sing Nat a -> Sing Nat b -> IsTrue ((Nat :<= Succ Nat a) b) -> (Ordering :~: Compare Nat a b) LT

leqZero :: Sing Nat n -> IsTrue ((Nat :<= Zero Nat) n)

leqSucc :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) m) -> IsTrue ((Nat :<= Succ Nat n) (Succ Nat m))

fromLeqView :: LeqView Nat n m -> IsTrue ((Nat :<= n) m)

leqViewRefl :: Sing Nat n -> LeqView Nat n n

viewLeq :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) m) -> LeqView Nat n m

leqWitness :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) m) -> DiffNat Nat n m

leqStep :: Sing Nat n -> Sing Nat m -> Sing Nat l -> (Nat :~: (Nat :+ n) l) m -> IsTrue ((Nat :<= n) m)

leqNeqToSuccLeq :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) m) -> ((Nat :~: n) m -> Void) -> IsTrue ((Nat :<= Succ Nat n) m)

leqRefl :: Sing Nat n -> IsTrue ((Nat :<= n) n)

leqSuccStepR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) m) -> IsTrue ((Nat :<= n) (Succ Nat m))

leqSuccStepL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= Succ Nat n) m) -> IsTrue ((Nat :<= n) m)

leqReflexive :: Sing Nat n -> Sing Nat m -> (Nat :~: n) m -> IsTrue ((Nat :<= n) m)

leqTrans :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat :<= n) m) -> IsTrue ((Nat :<= m) l) -> IsTrue ((Nat :<= n) l)

leqAntisymm :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) m) -> IsTrue ((Nat :<= m) n) -> (Nat :~: n) m

plusMonotone :: Sing Nat n -> Sing Nat m -> Sing Nat l -> Sing Nat k -> IsTrue ((Nat :<= n) m) -> IsTrue ((Nat :<= l) k) -> IsTrue ((Nat :<= (Nat :+ n) l) ((Nat :+ m) k))

leqZeroElim :: Sing Nat n -> IsTrue ((Nat :<= n) (Zero Nat)) -> (Nat :~: n) (Zero Nat)

plusMonotoneL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat :<= n) m) -> IsTrue ((Nat :<= (Nat :+ n) l) ((Nat :+ m) l))

plusMonotoneR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat :<= m) l) -> IsTrue ((Nat :<= (Nat :+ n) m) ((Nat :+ n) l))

plusLeqL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) ((Nat :+ n) m))

plusLeqR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= m) ((Nat :+ n) m))

plusCancelLeqR :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat :<= (Nat :+ n) l) ((Nat :+ m) l)) -> IsTrue ((Nat :<= n) m)

plusCancelLeqL :: Sing Nat n -> Sing Nat m -> Sing Nat l -> IsTrue ((Nat :<= (Nat :+ n) m) ((Nat :+ n) l)) -> IsTrue ((Nat :<= m) l)

succLeqZeroAbsurd :: Sing Nat n -> IsTrue ((Nat :<= S Nat n) (Zero Nat)) -> Void

succLeqZeroAbsurd' :: Sing Nat n -> (Bool :~: (Nat :<= S Nat n) (Zero Nat)) False

succLeqAbsurd :: Sing Nat n -> IsTrue ((Nat :<= S Nat n) n) -> Void

succLeqAbsurd' :: Sing Nat n -> (Bool :~: (Nat :<= S Nat n) n) False

notLeqToLeq :: (Bool ~ (Nat :<= n) m) False => Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= m) n)

leqSucc' :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat :<= n) m) ((Nat :<= Succ Nat n) (Succ Nat m))

leqToMin :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) m) -> (Nat :~: Min Nat n m) n

geqToMin :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= m) n) -> (Nat :~: Min Nat n m) m

minComm :: Sing Nat n -> Sing Nat m -> (Nat :~: Min Nat n m) (Min Nat m n)

minLeqL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= Min Nat n m) n)

minLeqR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= Min Nat n m) m)

minLargest :: Sing Nat l -> Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= l) n) -> IsTrue ((Nat :<= l) m) -> IsTrue ((Nat :<= l) (Min Nat n m))

leqToMax :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) m) -> (Nat :~: Max Nat n m) m

geqToMax :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= m) n) -> (Nat :~: Max Nat n m) n

maxComm :: Sing Nat n -> Sing Nat m -> (Nat :~: Max Nat n m) (Max Nat m n)

maxLeqR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= m) (Max Nat n m))

maxLeqL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) (Max Nat n m))

maxLeast :: Sing Nat l -> Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= n) l) -> IsTrue ((Nat :<= m) l) -> IsTrue ((Nat :<= Max Nat n m) l)

leqReversed :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat :<= n) m) ((Nat :>= m) n)

lneqSuccLeq :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat :< n) m) ((Nat :<= Succ Nat n) m)

lneqReversed :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat :< n) m) ((Nat :> m) n)

lneqToLT :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :< n) m) -> (Ordering :~: Compare Nat n m) LT

ltToLneq :: Sing Nat n -> Sing Nat m -> (Ordering :~: Compare Nat n m) LT -> IsTrue ((Nat :< n) m)

lneqZero :: Sing Nat a -> IsTrue ((Nat :< Zero Nat) (Succ Nat a))

lneqSucc :: Sing Nat n -> IsTrue ((Nat :< n) (Succ Nat n))

succLneqSucc :: Sing Nat n -> Sing Nat m -> (Bool :~: (Nat :< n) m) ((Nat :< Succ Nat n) (Succ Nat m))

lneqRightPredSucc :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :< n) m) -> (Nat :~: m) (Succ Nat (Pred Nat m))

lneqSuccStepL :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :< Succ Nat n) m) -> IsTrue ((Nat :< n) m)

lneqSuccStepR :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :< n) m) -> IsTrue ((Nat :< n) (Succ Nat m))

plusStrictMonotone :: Sing Nat n -> Sing Nat m -> Sing Nat l -> Sing Nat k -> IsTrue ((Nat :< n) m) -> IsTrue ((Nat :< l) k) -> IsTrue ((Nat :< (Nat :+ n) l) ((Nat :+ m) k))

maxZeroL :: Sing Nat n -> (Nat :~: Max Nat (Zero Nat) n) n

maxZeroR :: Sing Nat n -> (Nat :~: Max Nat n (Zero Nat)) n

minZeroL :: Sing Nat n -> (Nat :~: Min Nat (Zero Nat) n) (Zero Nat)

minZeroR :: Sing Nat n -> (Nat :~: Min Nat n (Zero Nat)) (Zero Nat)

minusSucc :: Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= m) n) -> (Nat :~: (Nat :- Succ Nat n) m) (Succ Nat ((Nat :- n) m))

lneqZeroAbsurd :: Sing Nat n -> IsTrue ((Nat :< n) (Zero Nat)) -> Void

minusPlus :: PeanoOrder Nat => Sing Nat n -> Sing Nat m -> IsTrue ((Nat :<= m) n) -> (Nat :~: (Nat :+ (Nat :- n) m) m) n

Monomorphicable Nat (Sing Nat)

Associated Types

type MonomorphicRep (Sing Nat) (k1 :: Sing Nat -> *) :: *

Methods

promote :: MonomorphicRep (Sing Nat) k1 -> Monomorphic (Sing Nat) k1

demote :: Monomorphic (Sing Nat) k1 -> MonomorphicRep (Sing Nat) k1