data-fin-0.1.1.3: Finite totally ordered sets

Portabilitynon-portable
Stabilityexperimental
Maintainerwren@community.haskell.org
Safe HaskellTrustworthy

Data.Number.Fin.TyDecimal

Contents

Description

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

Synopsis

Representation

Type-level decimal natural numbers

data D0 Source

The digit 0.

Instances

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) 

data D1 Source

The digit 1.

Instances

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) 

data D2 Source

The digit 2.

Instances

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) 

data D3 Source

The digit 3.

Instances

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) 

data D4 Source

The digit 4.

Instances

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) 

data D5 Source

The digit 5.

Instances

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) 

data D6 Source

The digit 6.

Instances

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) 

data D7 Source

The digit 7.

Instances

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) 

data D8 Source

The digit 8.

Instances

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) 

data D9 Source

The digit 9.

Instances

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) 

data x :. y Source

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.

Instances

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

data LT_ Source

Instances

Typeable LT_ 
Reifies * LT_ Ordering 
Compare D8 D9 LT_ 
Compare D7 D9 LT_ 
Compare D7 D8 LT_ 
Compare D6 D9 LT_ 
Compare D6 D8 LT_ 
Compare D6 D7 LT_ 
Compare D5 D9 LT_ 
Compare D5 D8 LT_ 
Compare D5 D7 LT_ 
Compare D5 D6 LT_ 
Compare D4 D9 LT_ 
Compare D4 D8 LT_ 
Compare D4 D7 LT_ 
Compare D4 D6 LT_ 
Compare D4 D5 LT_ 
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 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 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 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_ 
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_ 

data EQ_ Source

Instances

Typeable EQ_ 
Reifies * EQ_ Ordering 
Compare D9 D9 EQ_ 
Compare D8 D8 EQ_ 
Compare D7 D7 EQ_ 
Compare D6 D6 EQ_ 
Compare D5 D5 EQ_ 
Compare D4 D4 EQ_ 
Compare D3 D3 EQ_ 
Compare D2 D2 EQ_ 
Compare D1 D1 EQ_ 
Compare D0 D0 EQ_ 

data GT_ Source

Instances

Typeable GT_ 
Reifies * GT_ Ordering 
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 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 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 D5 GT_ 
Compare D6 D4 GT_ 
Compare D6 D3 GT_ 
Compare D6 D2 GT_ 
Compare D6 D1 GT_ 
Compare D6 D0 GT_ 
Compare D5 D4 GT_ 
Compare D5 D3 GT_ 
Compare D5 D2 GT_ 
Compare D5 D1 GT_ 
Compare D5 D0 GT_ 
Compare D4 D3 GT_ 
Compare D4 D2 GT_ 
Compare D4 D1 GT_ 
Compare D4 D0 GT_ 
Compare D3 D2 GT_ 
Compare D3 D1 GT_ 
Compare D3 D0 GT_ 
Compare D2 D1 GT_ 
Compare D2 D0 GT_ 
Compare D1 D0 GT_ 
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_ 

Kind predicates

class Nat_ n => Nat n Source

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).

Instances

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).

Instances

NatNE0_ n => NatNE0 n 

Proxies for some small numbers

nat0 :: Proxy D0Source

nat1 :: Proxy D1Source

nat2 :: Proxy D2Source

nat3 :: Proxy D3Source

nat4 :: Proxy D4Source

nat5 :: Proxy D5Source

nat6 :: Proxy D6Source

nat7 :: Proxy D7Source

nat8 :: Proxy D8Source

nat9 :: Proxy D9Source

Aliases for some large numbers

type MaxBoundInt8 = (D1 :. D2) :. D7Source

type MaxBoundInt16 = (((D3 :. D2) :. D7) :. D6) :. D7Source

type MaxBoundInt32 = ((((((((D2 :. D1) :. D4) :. D7) :. D4) :. D8) :. D3) :. D6) :. D4) :. D7Source

type MaxBoundInt64 = (((((((((((((((((D9 :. D2) :. D2) :. D3) :. D3) :. D7) :. D2) :. D0) :. D3) :. D6) :. D8) :. D5) :. D4) :. D7) :. D7) :. D5) :. D8) :. D0) :. D7Source

type MaxBoundWord8 = (D2 :. D5) :. D5Source

type MaxBoundWord16 = (((D6 :. D5) :. D5) :. D3) :. D5Source

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

Instances

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) 

succ :: Succ x y => Proxy x -> Proxy ySource

pred :: Succ x y => Proxy y -> Proxy xSource

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.

Instances

(Add_ x y z, Add_ y x z) => Add x y z 

add :: Add x y z => Proxy x -> Proxy y -> Proxy zSource

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.

Instances

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 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 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 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 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 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 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 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 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 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) => 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 dx), NatNE0_ (:. y dy), Compare dx dy dr, Compare x y r', NCS r' dr r) => Compare (:. x dx) (:. y dy) r 

compare :: Compare x y r => Proxy x -> Proxy y -> Proxy rSource

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.

Instances

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.

Instances

(Succ y' y, NatLE x y') => NatLT x y 

assert_NatLE :: NatLE x y => Proxy x -> Proxy y -> ()Source

N.B., this will be ill-typed if x is greater than y.

min :: (Compare x y r, Min_ x y r z) => Proxy x -> Proxy y -> Proxy zSource

Choose the smaller of x and y.

max :: (Compare x y r, Max_ x y r z) => Proxy x -> Proxy y -> Proxy zSource

Choose the larger of x and y.