linear-maps-0.5: Finite maps for linear useSource codeContentsIndex
Predefined values
Conversion to Int
Very simple type-level integers
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
data Zero Source
Zero represents 0 at the type level
show/hide Instances
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.
show/hide Instances
I a => I (Succ a)
Predefined values
type I0 = ZeroSource
type I1 = Succ I0Source
type I2 = Succ I1Source
type I3 = Succ I2Source
type I4 = Succ I3Source
type I5 = Succ I4Source
type I6 = Succ I5Source
type I7 = Succ I6Source
type I8 = Succ I7Source
type I9 = Succ I8Source
type I10 = Succ I9Source
type I11 = Succ I10Source
type I12 = Succ I11Source
type I13 = Succ I12Source
type I14 = Succ I13Source
type I15 = Succ I14Source
type I16 = Succ I15Source
type I17 = Succ I16Source
type I18 = Succ I17Source
type I19 = Succ I18Source
type I20 = Succ I19Source
type I21 = Succ I20Source
type I22 = Succ I21Source
type I23 = Succ I22Source
type I24 = Succ I23Source
type I25 = Succ I24Source
type I26 = Succ I25Source
type I27 = Succ I26Source
type I28 = Succ I27Source
type I29 = Succ I28Source
type I30 = Succ I29Source
type I31 = Succ I30Source
type I32 = Succ I31Source
Conversion to Int
class I m whereSource
Conversion to Int is achieved by the I type class.
num :: m -> IntSource
induction :: m -> a -> (a -> a) -> aSource
induction' :: a Zero -> (forall i. a i -> a (Succ i)) -> a mSource
induction'' :: a Zero x -> (forall i. a i x -> a (Succ i) x) -> a m xSource
show/hide Instances
I Zero
I a => I (Succ a)
Produced by Haddock version 2.4.2