Portability | non-portable |
---|---|
Stability | experimental |
Maintainer | wren@community.haskell.org |
Safe Haskell | Trustworthy |
Type-level decimal natural numbers. This is based on [1], and is
intended to work with [2] (though we use the reflection
package
for the actual reification part).
Recent versions of GHC have type-level natural number literals.
Ideally, this module would be completely obviated by that work.
Unfortunately, the type-level literals aren't quite ready for
prime time yet, because they do not have a solver. Thus, we're
implementing here stuff that should be handled natively by GHC
in the future. A lot of this also duplicates the functionality
in HList:Data.HList.FakePrelude
[3], which is (or should be)
obviated by the new data kinds extension.
- 1
- Oleg Kiselyov and Chung-chieh Shan. (2007) Lightweight static resources: Sexy types for embedded and systems programming. Proc. Trends in Functional Programming. New York, 2--4 April 2007. http://okmij.org/ftp/Haskell/types.html#binary-arithm
- 2
- Oleg Kiselyov and Chung-chieh Shan. (2004) Implicit configurations: or, type classes reflect the values of types. Proc. ACM SIGPLAN 2004 workshop on Haskell. Snowbird, Utah, USA, 22 September 2004. pp.33--44. http://okmij.org/ftp/Haskell/types.html#Prepose
- 3
- http://hackage.haskell.org/package/HList
- data D0
- data D1
- data D2
- data D3
- data D4
- data D5
- data D6
- data D7
- data D8
- data D9
- data x :. y
- data LT_
- data EQ_
- data GT_
- class Nat_ n => Nat n
- class NatNE0_ n => NatNE0 n
- nat0 :: Proxy D0
- nat1 :: Proxy D1
- nat2 :: Proxy D2
- nat3 :: Proxy D3
- nat4 :: Proxy D4
- nat5 :: Proxy D5
- nat6 :: Proxy D6
- nat7 :: Proxy D7
- nat8 :: Proxy D8
- nat9 :: Proxy D9
- type MaxBoundInt8 = (D1 :. D2) :. D7
- type MaxBoundInt16 = (((D3 :. D2) :. D7) :. D6) :. D7
- type MaxBoundInt32 = ((((((((D2 :. D1) :. D4) :. D7) :. D4) :. D8) :. D3) :. D6) :. D4) :. D7
- type MaxBoundInt64 = (((((((((((((((((D9 :. D2) :. D2) :. D3) :. D3) :. D7) :. D2) :. D0) :. D3) :. D6) :. D8) :. D5) :. D4) :. D7) :. D7) :. D5) :. D8) :. D0) :. D7
- type MaxBoundWord8 = (D2 :. D5) :. D5
- type MaxBoundWord16 = (((D6 :. D5) :. D5) :. D3) :. D5
- type MaxBoundWord32 = ((((((((D4 :. D2) :. D9) :. D4) :. D9) :. D6) :. D7) :. D2) :. D9) :. D5
- type MaxBoundWord64 = ((((((((((((((((((D1 :. D8) :. D4) :. D4) :. D6) :. D7) :. D4) :. D4) :. D0) :. D7) :. D3) :. D7) :. D0) :. D9) :. D5) :. D5) :. D1) :. D6) :. D1) :. D5
- class (Nat_ x, NatNE0_ y) => Succ x y | x -> y, y -> x
- succ :: Succ x y => Proxy x -> Proxy y
- pred :: Succ x y => Proxy y -> Proxy x
- class (Add_ x y z, Add_ y x z) => Add x y z | x y -> z, z x -> y, z y -> x
- add :: Add x y z => Proxy x -> Proxy y -> Proxy z
- minus :: Add x y z => Proxy z -> Proxy x -> Proxy y
- subtract :: Add x y z => Proxy x -> Proxy z -> Proxy y
- class (Nat_ x, Nat_ y) => Compare x y r | x y -> r
- compare :: Compare x y r => Proxy x -> Proxy y -> Proxy r
- class (Nat_ x, Nat_ y) => NatLE x y
- class (Nat_ x, NatNE0_ y) => NatLT x y
- assert_NatLE :: NatLE x y => Proxy x -> Proxy y -> ()
- min :: (Compare x y r, Min_ x y r z) => Proxy x -> Proxy y -> Proxy z
- max :: (Compare x y r, Max_ x y r z) => Proxy x -> Proxy y -> Proxy z
Representation
Type-level decimal natural numbers
The digit 0.
Typeable D0 | |
NatLE D0 D9 | |
NatLE D0 D8 | |
NatLE D0 D7 | |
NatLE D0 D6 | |
NatLE D0 D5 | |
NatLE D0 D4 | |
NatLE D0 D3 | |
NatLE D0 D2 | |
NatLE D0 D1 | |
NatLE D0 D0 | |
Succ D0 D1 | |
Reifies * D0 Integer | |
Compare D9 D0 GT_ | |
Compare D8 D0 GT_ | |
Compare D7 D0 GT_ | |
Compare D6 D0 GT_ | |
Compare D5 D0 GT_ | |
Compare D4 D0 GT_ | |
Compare D3 D0 GT_ | |
Compare D2 D0 GT_ | |
Compare D1 D0 GT_ | |
Compare D0 D9 LT_ | |
Compare D0 D8 LT_ | |
Compare D0 D7 LT_ | |
Compare D0 D6 LT_ | |
Compare D0 D5 LT_ | |
Compare D0 D4 LT_ | |
Compare D0 D3 LT_ | |
Compare D0 D2 LT_ | |
Compare D0 D1 LT_ | |
Compare D0 D0 EQ_ | |
NatNE0_ (:. y dy) => NatLE D0 (:. y dy) | |
Succ D9 (:. D1 D0) | |
NatNE0_ x => Reifies * (:. x D0) Integer | |
NatNE0_ (:. y dy) => Compare D0 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D0 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D2) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D1) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D0) | |
(NatNE0_ x, Succ x (:. y d)) => Succ (:. x D9) (:. (:. y d) D0) | |
NatNE0_ x => Succ (:. x D0) (:. x D1) |
The digit 1.
Typeable D1 | |
NatLE D1 D9 | |
NatLE D1 D8 | |
NatLE D1 D7 | |
NatLE D1 D6 | |
NatLE D1 D5 | |
NatLE D1 D4 | |
NatLE D1 D3 | |
NatLE D1 D2 | |
NatLE D1 D1 | |
NatLE D0 D1 | |
Succ D1 D2 | |
Succ D0 D1 | |
Reifies * D1 Integer | |
Compare D9 D1 GT_ | |
Compare D8 D1 GT_ | |
Compare D7 D1 GT_ | |
Compare D6 D1 GT_ | |
Compare D5 D1 GT_ | |
Compare D4 D1 GT_ | |
Compare D3 D1 GT_ | |
Compare D2 D1 GT_ | |
Compare D1 D9 LT_ | |
Compare D1 D8 LT_ | |
Compare D1 D7 LT_ | |
Compare D1 D6 LT_ | |
Compare D1 D5 LT_ | |
Compare D1 D4 LT_ | |
Compare D1 D3 LT_ | |
Compare D1 D2 LT_ | |
Compare D1 D1 EQ_ | |
Compare D1 D0 GT_ | |
Compare D0 D1 LT_ | |
NatNE0_ (:. y dy) => NatLE D1 (:. y dy) | |
Succ D9 (:. D1 D0) | |
NatNE0_ x => Reifies * (:. x D1) Integer | |
NatNE0_ (:. y dy) => Compare D1 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D1 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D2) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D1) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D1) | |
NatNE0_ x => Succ (:. x D1) (:. x D2) | |
NatNE0_ x => Succ (:. x D0) (:. x D1) |
The digit 2.
Typeable D2 | |
NatLE D2 D9 | |
NatLE D2 D8 | |
NatLE D2 D7 | |
NatLE D2 D6 | |
NatLE D2 D5 | |
NatLE D2 D4 | |
NatLE D2 D3 | |
NatLE D2 D2 | |
NatLE D1 D2 | |
NatLE D0 D2 | |
Succ D2 D3 | |
Succ D1 D2 | |
Reifies * D2 Integer | |
Compare D9 D2 GT_ | |
Compare D8 D2 GT_ | |
Compare D7 D2 GT_ | |
Compare D6 D2 GT_ | |
Compare D5 D2 GT_ | |
Compare D4 D2 GT_ | |
Compare D3 D2 GT_ | |
Compare D2 D9 LT_ | |
Compare D2 D8 LT_ | |
Compare D2 D7 LT_ | |
Compare D2 D6 LT_ | |
Compare D2 D5 LT_ | |
Compare D2 D4 LT_ | |
Compare D2 D3 LT_ | |
Compare D2 D2 EQ_ | |
Compare D2 D1 GT_ | |
Compare D2 D0 GT_ | |
Compare D1 D2 LT_ | |
Compare D0 D2 LT_ | |
NatNE0_ (:. y dy) => NatLE D2 (:. y dy) | |
NatNE0_ x => Reifies * (:. x D2) Integer | |
NatNE0_ (:. y dy) => Compare D2 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D2 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D2) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D2) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D2) | |
NatNE0_ x => Succ (:. x D2) (:. x D3) | |
NatNE0_ x => Succ (:. x D1) (:. x D2) |
The digit 3.
Typeable D3 | |
NatLE D3 D9 | |
NatLE D3 D8 | |
NatLE D3 D7 | |
NatLE D3 D6 | |
NatLE D3 D5 | |
NatLE D3 D4 | |
NatLE D3 D3 | |
NatLE D2 D3 | |
NatLE D1 D3 | |
NatLE D0 D3 | |
Succ D3 D4 | |
Succ D2 D3 | |
Reifies * D3 Integer | |
Compare D9 D3 GT_ | |
Compare D8 D3 GT_ | |
Compare D7 D3 GT_ | |
Compare D6 D3 GT_ | |
Compare D5 D3 GT_ | |
Compare D4 D3 GT_ | |
Compare D3 D9 LT_ | |
Compare D3 D8 LT_ | |
Compare D3 D7 LT_ | |
Compare D3 D6 LT_ | |
Compare D3 D5 LT_ | |
Compare D3 D4 LT_ | |
Compare D3 D3 EQ_ | |
Compare D3 D2 GT_ | |
Compare D3 D1 GT_ | |
Compare D3 D0 GT_ | |
Compare D2 D3 LT_ | |
Compare D1 D3 LT_ | |
Compare D0 D3 LT_ | |
NatNE0_ (:. y dy) => NatLE D3 (:. y dy) | |
NatNE0_ x => Reifies * (:. x D3) Integer | |
NatNE0_ (:. y dy) => Compare D3 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D3 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D3) | |
NatNE0_ x => Succ (:. x D3) (:. x D4) | |
NatNE0_ x => Succ (:. x D2) (:. x D3) |
The digit 4.
Typeable D4 | |
NatLE D4 D9 | |
NatLE D4 D8 | |
NatLE D4 D7 | |
NatLE D4 D6 | |
NatLE D4 D5 | |
NatLE D4 D4 | |
NatLE D3 D4 | |
NatLE D2 D4 | |
NatLE D1 D4 | |
NatLE D0 D4 | |
Succ D4 D5 | |
Succ D3 D4 | |
Reifies * D4 Integer | |
Compare D9 D4 GT_ | |
Compare D8 D4 GT_ | |
Compare D7 D4 GT_ | |
Compare D6 D4 GT_ | |
Compare D5 D4 GT_ | |
Compare D4 D9 LT_ | |
Compare D4 D8 LT_ | |
Compare D4 D7 LT_ | |
Compare D4 D6 LT_ | |
Compare D4 D5 LT_ | |
Compare D4 D4 EQ_ | |
Compare D4 D3 GT_ | |
Compare D4 D2 GT_ | |
Compare D4 D1 GT_ | |
Compare D4 D0 GT_ | |
Compare D3 D4 LT_ | |
Compare D2 D4 LT_ | |
Compare D1 D4 LT_ | |
Compare D0 D4 LT_ | |
NatNE0_ (:. y dy) => NatLE D4 (:. y dy) | |
NatNE0_ x => Reifies * (:. x D4) Integer | |
NatNE0_ (:. y dy) => Compare D4 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D4 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D4) | |
NatNE0_ x => Succ (:. x D4) (:. x D5) | |
NatNE0_ x => Succ (:. x D3) (:. x D4) |
The digit 5.
Typeable D5 | |
NatLE D5 D9 | |
NatLE D5 D8 | |
NatLE D5 D7 | |
NatLE D5 D6 | |
NatLE D5 D5 | |
NatLE D4 D5 | |
NatLE D3 D5 | |
NatLE D2 D5 | |
NatLE D1 D5 | |
NatLE D0 D5 | |
Succ D5 D6 | |
Succ D4 D5 | |
Reifies * D5 Integer | |
Compare D9 D5 GT_ | |
Compare D8 D5 GT_ | |
Compare D7 D5 GT_ | |
Compare D6 D5 GT_ | |
Compare D5 D9 LT_ | |
Compare D5 D8 LT_ | |
Compare D5 D7 LT_ | |
Compare D5 D6 LT_ | |
Compare D5 D5 EQ_ | |
Compare D5 D4 GT_ | |
Compare D5 D3 GT_ | |
Compare D5 D2 GT_ | |
Compare D5 D1 GT_ | |
Compare D5 D0 GT_ | |
Compare D4 D5 LT_ | |
Compare D3 D5 LT_ | |
Compare D2 D5 LT_ | |
Compare D1 D5 LT_ | |
Compare D0 D5 LT_ | |
NatNE0_ (:. y dy) => NatLE D5 (:. y dy) | |
NatNE0_ x => Reifies * (:. x D5) Integer | |
NatNE0_ (:. y dy) => Compare D5 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D5 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D5) | |
NatNE0_ x => Succ (:. x D5) (:. x D6) | |
NatNE0_ x => Succ (:. x D4) (:. x D5) |
The digit 6.
Typeable D6 | |
NatLE D6 D9 | |
NatLE D6 D8 | |
NatLE D6 D7 | |
NatLE D6 D6 | |
NatLE D5 D6 | |
NatLE D4 D6 | |
NatLE D3 D6 | |
NatLE D2 D6 | |
NatLE D1 D6 | |
NatLE D0 D6 | |
Succ D6 D7 | |
Succ D5 D6 | |
Reifies * D6 Integer | |
Compare D9 D6 GT_ | |
Compare D8 D6 GT_ | |
Compare D7 D6 GT_ | |
Compare D6 D9 LT_ | |
Compare D6 D8 LT_ | |
Compare D6 D7 LT_ | |
Compare D6 D6 EQ_ | |
Compare D6 D5 GT_ | |
Compare D6 D4 GT_ | |
Compare D6 D3 GT_ | |
Compare D6 D2 GT_ | |
Compare D6 D1 GT_ | |
Compare D6 D0 GT_ | |
Compare D5 D6 LT_ | |
Compare D4 D6 LT_ | |
Compare D3 D6 LT_ | |
Compare D2 D6 LT_ | |
Compare D1 D6 LT_ | |
Compare D0 D6 LT_ | |
NatNE0_ (:. y dy) => NatLE D6 (:. y dy) | |
NatNE0_ x => Reifies * (:. x D6) Integer | |
NatNE0_ (:. y dy) => Compare D6 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D6 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D6) | |
NatNE0_ x => Succ (:. x D6) (:. x D7) | |
NatNE0_ x => Succ (:. x D5) (:. x D6) |
The digit 7.
Typeable D7 | |
NatLE D7 D9 | |
NatLE D7 D8 | |
NatLE D7 D7 | |
NatLE D6 D7 | |
NatLE D5 D7 | |
NatLE D4 D7 | |
NatLE D3 D7 | |
NatLE D2 D7 | |
NatLE D1 D7 | |
NatLE D0 D7 | |
Succ D7 D8 | |
Succ D6 D7 | |
Reifies * D7 Integer | |
Compare D9 D7 GT_ | |
Compare D8 D7 GT_ | |
Compare D7 D9 LT_ | |
Compare D7 D8 LT_ | |
Compare D7 D7 EQ_ | |
Compare D7 D6 GT_ | |
Compare D7 D5 GT_ | |
Compare D7 D4 GT_ | |
Compare D7 D3 GT_ | |
Compare D7 D2 GT_ | |
Compare D7 D1 GT_ | |
Compare D7 D0 GT_ | |
Compare D6 D7 LT_ | |
Compare D5 D7 LT_ | |
Compare D4 D7 LT_ | |
Compare D3 D7 LT_ | |
Compare D2 D7 LT_ | |
Compare D1 D7 LT_ | |
Compare D0 D7 LT_ | |
NatNE0_ (:. y dy) => NatLE D7 (:. y dy) | |
NatNE0_ x => Reifies * (:. x D7) Integer | |
NatNE0_ (:. y dy) => Compare D7 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D7 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D7) | |
NatNE0_ x => Succ (:. x D7) (:. x D8) | |
NatNE0_ x => Succ (:. x D6) (:. x D7) |
The digit 8.
Typeable D8 | |
NatLE D8 D9 | |
NatLE D8 D8 | |
NatLE D7 D8 | |
NatLE D6 D8 | |
NatLE D5 D8 | |
NatLE D4 D8 | |
NatLE D3 D8 | |
NatLE D2 D8 | |
NatLE D1 D8 | |
NatLE D0 D8 | |
Succ D8 D9 | |
Succ D7 D8 | |
Reifies * D8 Integer | |
Compare D9 D8 GT_ | |
Compare D8 D9 LT_ | |
Compare D8 D8 EQ_ | |
Compare D8 D7 GT_ | |
Compare D8 D6 GT_ | |
Compare D8 D5 GT_ | |
Compare D8 D4 GT_ | |
Compare D8 D3 GT_ | |
Compare D8 D2 GT_ | |
Compare D8 D1 GT_ | |
Compare D8 D0 GT_ | |
Compare D7 D8 LT_ | |
Compare D6 D8 LT_ | |
Compare D5 D8 LT_ | |
Compare D4 D8 LT_ | |
Compare D3 D8 LT_ | |
Compare D2 D8 LT_ | |
Compare D1 D8 LT_ | |
Compare D0 D8 LT_ | |
NatNE0_ (:. y dy) => NatLE D8 (:. y dy) | |
NatNE0_ x => Reifies * (:. x D8) Integer | |
NatNE0_ (:. y dy) => Compare D8 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D8 GT_ | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D8) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D8) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D8) | |
NatNE0_ x => Succ (:. x D8) (:. x D9) | |
NatNE0_ x => Succ (:. x D7) (:. x D8) |
The digit 9.
Typeable D9 | |
NatLE D9 D9 | |
NatLE D8 D9 | |
NatLE D7 D9 | |
NatLE D6 D9 | |
NatLE D5 D9 | |
NatLE D4 D9 | |
NatLE D3 D9 | |
NatLE D2 D9 | |
NatLE D1 D9 | |
NatLE D0 D9 | |
Succ D8 D9 | |
Reifies * D9 Integer | |
Compare D9 D9 EQ_ | |
Compare D9 D8 GT_ | |
Compare D9 D7 GT_ | |
Compare D9 D6 GT_ | |
Compare D9 D5 GT_ | |
Compare D9 D4 GT_ | |
Compare D9 D3 GT_ | |
Compare D9 D2 GT_ | |
Compare D9 D1 GT_ | |
Compare D9 D0 GT_ | |
Compare D8 D9 LT_ | |
Compare D7 D9 LT_ | |
Compare D6 D9 LT_ | |
Compare D5 D9 LT_ | |
Compare D4 D9 LT_ | |
Compare D3 D9 LT_ | |
Compare D2 D9 LT_ | |
Compare D1 D9 LT_ | |
Compare D0 D9 LT_ | |
NatNE0_ (:. y dy) => NatLE D9 (:. y dy) | |
Succ D9 (:. D1 D0) | |
NatNE0_ x => Reifies * (:. x D9) Integer | |
NatNE0_ (:. y dy) => Compare D9 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D9 GT_ | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D9) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D8) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D9) | |
(NatNE0_ x, Succ x (:. y d)) => Succ (:. x D9) (:. (:. y d) D0) | |
NatNE0_ x => Succ (:. x D8) (:. x D9) |
The connective. This should only be used left associatively (it associates to the left naturally). Decimal digits are lexicographically big-endian, so they're written as usual; however, they're structurally little-endian due to the left associativity.
Typeable2 :. | |
NatNE0_ (:. y dy) => NatLE D9 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D8 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D7 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D6 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D5 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D4 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D3 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D2 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D1 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D0 (:. y dy) | |
Succ D9 (:. D1 D0) | |
NatNE0_ x => Reifies * (:. x D9) Integer | |
NatNE0_ x => Reifies * (:. x D8) Integer | |
NatNE0_ x => Reifies * (:. x D7) Integer | |
NatNE0_ x => Reifies * (:. x D6) Integer | |
NatNE0_ x => Reifies * (:. x D5) Integer | |
NatNE0_ x => Reifies * (:. x D4) Integer | |
NatNE0_ x => Reifies * (:. x D3) Integer | |
NatNE0_ x => Reifies * (:. x D2) Integer | |
NatNE0_ x => Reifies * (:. x D1) Integer | |
NatNE0_ x => Reifies * (:. x D0) Integer | |
NatNE0_ (:. y dy) => Compare D9 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D8 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D7 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D6 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D5 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D4 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D3 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D2 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D1 (:. y dy) LT_ | |
NatNE0_ (:. y dy) => Compare D0 (:. y dy) LT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D9 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D8 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D7 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D6 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D5 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D4 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D3 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D2 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D1 GT_ | |
NatNE0_ (:. x dx) => Compare (:. x dx) D0 GT_ | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D9) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D8) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D8) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D2) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D2) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D1) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D0) | |
(NatNE0_ x, Succ x (:. y d)) => Succ (:. x D9) (:. (:. y d) D0) | |
NatNE0_ x => Succ (:. x D8) (:. x D9) | |
NatNE0_ x => Succ (:. x D7) (:. x D8) | |
NatNE0_ x => Succ (:. x D6) (:. x D7) | |
NatNE0_ x => Succ (:. x D5) (:. x D6) | |
NatNE0_ x => Succ (:. x D4) (:. x D5) | |
NatNE0_ x => Succ (:. x D3) (:. x D4) | |
NatNE0_ x => Succ (:. x D2) (:. x D3) | |
NatNE0_ x => Succ (:. x D1) (:. x D2) | |
NatNE0_ x => Succ (:. x D0) (:. x D1) | |
(NatNE0_ (:. x dx), NatNE0_ (:. y dy), Compare dx dy dr, Compare x y r', NCS r' dr r) => Compare (:. x dx) (:. y dy) r |
Type-level Ordering
Kind predicates
Is n
a well-formed type of kind Nat
? The only well-formed
types of kind Nat
are type-level natural numbers in structurally
little-endian decimal.
The hidden type class (Nat_ n)
entails (Reifies n Integer)
.
Nat_ n => Nat n |
class NatNE0_ n => NatNE0 n Source
Is n
a well-formed type of kind NatNE0
? The only well-formed
types of kind NatNE0
are the non-zero well-formed types of
kind Nat
;, i.e., the type-level whole numbers in structurally
little-endian decimal.
The hidden type class (NatNE0_ n)
entails (Nat_ n)
and
(Reifies n Integer)
.
NatNE0_ n => NatNE0 n |
Proxies for some small numbers
Aliases for some large numbers
type MaxBoundInt64 = (((((((((((((((((D9 :. D2) :. D2) :. D3) :. D3) :. D7) :. D2) :. D0) :. D3) :. D6) :. D8) :. D5) :. D4) :. D7) :. D7) :. D5) :. D8) :. D0) :. D7Source
type MaxBoundWord32 = ((((((((D4 :. D2) :. D9) :. D4) :. D9) :. D6) :. D7) :. D2) :. D9) :. D5Source
type MaxBoundWord64 = ((((((((((((((((((D1 :. D8) :. D4) :. D4) :. D6) :. D7) :. D4) :. D4) :. D0) :. D7) :. D3) :. D7) :. D0) :. D9) :. D5) :. D5) :. D1) :. D6) :. D1) :. D5Source
Arithmetic
successor/predecessor
class (Nat_ x, NatNE0_ y) => Succ x y | x -> y, y -> xSource
The successor/predecessor relation; by structural induction on the first argument. Modes:
Succ x (succ x) -- i.e., given x, return the successor of x Succ (pred y) y -- i.e., given y, return the predecessor of y
Succ D8 D9 | |
Succ D7 D8 | |
Succ D6 D7 | |
Succ D5 D6 | |
Succ D4 D5 | |
Succ D3 D4 | |
Succ D2 D3 | |
Succ D1 D2 | |
Succ D0 D1 | |
Succ D9 (:. D1 D0) | |
(NatNE0_ x, Succ x (:. y d)) => Succ (:. x D9) (:. (:. y d) D0) | |
NatNE0_ x => Succ (:. x D8) (:. x D9) | |
NatNE0_ x => Succ (:. x D7) (:. x D8) | |
NatNE0_ x => Succ (:. x D6) (:. x D7) | |
NatNE0_ x => Succ (:. x D5) (:. x D6) | |
NatNE0_ x => Succ (:. x D4) (:. x D5) | |
NatNE0_ x => Succ (:. x D3) (:. x D4) | |
NatNE0_ x => Succ (:. x D2) (:. x D3) | |
NatNE0_ x => Succ (:. x D1) (:. x D2) | |
NatNE0_ x => Succ (:. x D0) (:. x D1) |
addition/subtraction
class (Add_ x y z, Add_ y x z) => Add x y z | x y -> z, z x -> y, z y -> xSource
The addition relation with full dependencies. Modes:
Add x y (x+y) Add x (z-x) z -- when it's defined. Add (z-y) y z -- when it's defined.
(Add_ x y z, Add_ y x z) => Add x y z |
minus :: Add x y z => Proxy z -> Proxy x -> Proxy ySource
N.B., this will be ill-typed if x
is greater than z
.
subtract :: Add x y z => Proxy x -> Proxy z -> Proxy ySource
N.B., this will be ill-typed if x
is greater than z
.
comparison
class (Nat_ x, Nat_ y) => Compare x y r | x y -> rSource
Assert that the comparison relation r
(LT_
, EQ_
, or
GT_
) holds between x
and y
; by structural induction on the
first, and then the second argument.
class (Nat_ x, Nat_ y) => NatLE x y Source
Assert that x <= y
. This is a popular constraint, so we
implement it specially. We could have said that Add n x y =>
NatLE x y
, but the following inductive definition is a bit
more optimal.
NatLE D9 D9 | |
NatLE D8 D9 | |
NatLE D8 D8 | |
NatLE D7 D9 | |
NatLE D7 D8 | |
NatLE D7 D7 | |
NatLE D6 D9 | |
NatLE D6 D8 | |
NatLE D6 D7 | |
NatLE D6 D6 | |
NatLE D5 D9 | |
NatLE D5 D8 | |
NatLE D5 D7 | |
NatLE D5 D6 | |
NatLE D5 D5 | |
NatLE D4 D9 | |
NatLE D4 D8 | |
NatLE D4 D7 | |
NatLE D4 D6 | |
NatLE D4 D5 | |
NatLE D4 D4 | |
NatLE D3 D9 | |
NatLE D3 D8 | |
NatLE D3 D7 | |
NatLE D3 D6 | |
NatLE D3 D5 | |
NatLE D3 D4 | |
NatLE D3 D3 | |
NatLE D2 D9 | |
NatLE D2 D8 | |
NatLE D2 D7 | |
NatLE D2 D6 | |
NatLE D2 D5 | |
NatLE D2 D4 | |
NatLE D2 D3 | |
NatLE D2 D2 | |
NatLE D1 D9 | |
NatLE D1 D8 | |
NatLE D1 D7 | |
NatLE D1 D6 | |
NatLE D1 D5 | |
NatLE D1 D4 | |
NatLE D1 D3 | |
NatLE D1 D2 | |
NatLE D1 D1 | |
NatLE D0 D9 | |
NatLE D0 D8 | |
NatLE D0 D7 | |
NatLE D0 D6 | |
NatLE D0 D5 | |
NatLE D0 D4 | |
NatLE D0 D3 | |
NatLE D0 D2 | |
NatLE D0 D1 | |
NatLE D0 D0 | |
NatNE0_ (:. y dy) => NatLE D9 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D8 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D7 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D6 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D5 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D4 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D3 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D2 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D1 (:. y dy) | |
NatNE0_ (:. y dy) => NatLE D0 (:. y dy) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D9) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D9) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D8) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D8) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D8) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D7) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D7) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D6) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D6) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D5) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D5) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D4) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D4) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D3) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D3) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D2) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D2) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D2) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D1) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (:. x D1) (:. y D0) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D9) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D8) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D7) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D6) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D5) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D4) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D3) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D2) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D1) | |
(NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (:. x D0) (:. y D0) |
class (Nat_ x, NatNE0_ y) => NatLT x y Source
Assert that x < y
. This is just a shorthand for x <= pred y
.
assert_NatLE :: NatLE x y => Proxy x -> Proxy y -> ()Source
N.B., this will be ill-typed if x
is greater than y
.