Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell98 |
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
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) |
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) |
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) |