Data.TypeInt
 Contents Constructors Predefined values Conversion to Int
Description
Very simple type-level integers
Synopsis
data Zero
data Succ a
type I0 = Zero
type I1 = Succ I0
type I2 = Succ I1
type I3 = Succ I2
type I4 = Succ I3
type I5 = Succ I4
type I6 = Succ I5
type I7 = Succ I6
type I8 = Succ I7
type I9 = Succ I8
type I10 = Succ I9
type I11 = Succ I10
type I12 = Succ I11
type I13 = Succ I12
type I14 = Succ I13
type I15 = Succ I14
type I16 = Succ I15
type I17 = Succ I16
type I18 = Succ I17
type I19 = Succ I18
type I20 = Succ I19
type I21 = Succ I20
type I22 = Succ I21
type I23 = Succ I22
type I24 = Succ I23
type I25 = Succ I24
type I26 = Succ I25
type I27 = Succ I26
type I28 = Succ I27
type I29 = Succ I28
type I30 = Succ I29
type I31 = Succ I30
type I32 = Succ I31
class I m where
 num :: m -> Int induction :: m -> a -> (a -> a) -> a induction' :: a Zero -> (forall i. a i -> a (Succ i)) -> a m induction'' :: a Zero x -> (forall i. a i x -> a (Succ i) x) -> a m x
Constructors
 data Zero Source
Zero represents 0 at the type level
Instances
 I Zero
 data Succ a Source
If a represents the natural number n at the type level then (Succ a) represents (1 + n) at the type level.
Instances
 I a => I (Succ a)
Predefined values
 type I0 = Zero Source
 type I1 = Succ I0 Source
 type I2 = Succ I1 Source
 type I3 = Succ I2 Source
 type I4 = Succ I3 Source
 type I5 = Succ I4 Source
 type I6 = Succ I5 Source
 type I7 = Succ I6 Source
 type I8 = Succ I7 Source
 type I9 = Succ I8 Source
 type I10 = Succ I9 Source
 type I11 = Succ I10 Source
 type I12 = Succ I11 Source
 type I13 = Succ I12 Source
 type I14 = Succ I13 Source
 type I15 = Succ I14 Source
 type I16 = Succ I15 Source
 type I17 = Succ I16 Source
 type I18 = Succ I17 Source
 type I19 = Succ I18 Source
 type I20 = Succ I19 Source
 type I21 = Succ I20 Source
 type I22 = Succ I21 Source
 type I23 = Succ I22 Source
 type I24 = Succ I23 Source
 type I25 = Succ I24 Source
 type I26 = Succ I25 Source
 type I27 = Succ I26 Source
 type I28 = Succ I27 Source
 type I29 = Succ I28 Source
 type I30 = Succ I29 Source
 type I31 = Succ I30 Source
 type I32 = Succ I31 Source
Conversion to Int
 class I m where Source
Conversion to Int is achieved by the I type class.
Methods
 num :: m -> Int Source
 induction :: m -> a -> (a -> a) -> a Source
 induction' :: a Zero -> (forall i. a i -> a (Succ i)) -> a m Source
 induction'' :: a Zero x -> (forall i. a i x -> a (Succ i) x) -> a m x Source
Instances
 I Zero I a => I (Succ a)
Produced by Haddock version 2.4.2