| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Data.Sized.Arith
Description
Basic type-level arithmetic, using base two.
Copyright: (c) 2009 University of Kansas License: BSD3
Maintainer: Andy Gill andygill@ku.edu Stability: unstable Portability: ghc
Documentation
Constructors
| X0 |
Instances
| Size a => Bounded (X0_ a) | |
| Size a => Enum (X0_ a) | |
| Eq (X0_ a) | |
| (Size a, Size (X0_ a), Integral a) => Integral (X0_ a) | |
| Size a => Num (X0_ a) | |
| Ord (X0_ a) | |
| Size a => Real (X0_ a) | |
| Show (X0_ a) | |
| Size a => Ix (X0_ a) | |
| Size a => Size (X0_ a) | |
| type MUL x (X0_ b) = ADD x (MUL x (ADD (X0_ b) N1)) | |
| type ADD N1 (X0_ b) = APP1 (ADD N1 b) | |
| type APP0 (X0_ a) = X0_ (X0_ a) | |
| type APP1 (X0_ a) = X1_ (X0_ a) | |
| type LOG (X0_ a) = ADD (X1_ X0) (LOG a) | |
| type SUCC (X0_ a) = APP1 a | |
| type NOT (X0_ a) = APP1 (NOT a) | |
| type Index (X0_ a) = Int | |
| type ADD (X0_ a) N1 = APP1 (ADD a N1) | |
| type ADD (X1_ a) (X0_ b) = APP1 (ADD a b) | |
| type ADD (X0_ a) (X1_ b) = APP1 (ADD a b) | |
| type ADD (X0_ a) (X0_ b) = APP0 (ADD a b) |
Instances
| Size a => Bounded (X1_ a) | |
| Size a => Enum (X1_ a) | |
| Eq (X1_ a) | |
| (Size a, Size (X1_ a), Integral a) => Integral (X1_ a) | |
| Size a => Num (X1_ a) | |
| Ord (X1_ a) | |
| Size a => Real (X1_ a) | |
| Show (X1_ a) | |
| Size a => Ix (X1_ a) | |
| Size a => Size (X1_ a) | |
| type MUL x (X1_ b) = ADD x (MUL x (ADD (X1_ b) N1)) | |
| type ADD N1 (X1_ b) = APP0 b | |
| type APP0 (X1_ a) = X0_ (X1_ a) | |
| type APP1 (X1_ a) = X1_ (X1_ a) | |
| type LOG (X1_ a) = ADD (X1_ X0) (LOG a) | |
| type SUCC (X1_ a) = APP0 (SUCC a) | |
| type NOT (X1_ a) = APP0 (NOT a) | |
| type Index (X1_ a) = Int | |
| type ADD (X1_ a) N1 = APP0 a | |
| type ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b)) | |
| type ADD (X1_ a) (X0_ b) = APP1 (ADD a b) | |
| type ADD (X0_ a) (X1_ b) = APP1 (ADD a b) |
Instances
| type ADD a X0 = a | |
| type ADD X0 a = a | |
| type ADD X0 N1 = N1 | |
| type ADD N1 N1 = APP0 N1 | |
| type ADD N1 (X1_ b) = APP0 b | |
| type ADD N1 (X0_ b) = APP1 (ADD N1 b) | |
| type ADD (X1_ a) N1 = APP0 a | |
| type ADD (X0_ a) N1 = APP1 (ADD a N1) | |
| type ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b)) | |
| type ADD (X1_ a) (X0_ b) = APP1 (ADD a b) | |
| type ADD (X0_ a) (X1_ b) = APP1 (ADD a b) | |
| type ADD (X0_ a) (X0_ b) = APP0 (ADD a b) |