%* | Data.Type.Natural |
%** | Data.Type.Natural |
%+ | Data.Type.Natural |
%- | Data.Type.Natural |
%:* | Data.Type.Natural |
%:** | Data.Type.Natural |
%:+ | Data.Type.Natural |
%:- | Data.Type.Natural |
%:-. | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
:* | Data.Type.Natural |
:*$ | Data.Type.Natural |
:*$$ | Data.Type.Natural |
:*$$$ | Data.Type.Natural |
:** | Data.Type.Natural |
:**: | Data.Type.Natural |
:*: | Data.Type.Natural |
:+ | Data.Type.Natural |
:+$ | Data.Type.Natural |
:+$$ | Data.Type.Natural |
:+$$$ | Data.Type.Natural |
:+: | Data.Type.Natural |
:- | Data.Type.Natural |
:-$ | Data.Type.Natural |
:-$$ | Data.Type.Natural |
:-$$$ | Data.Type.Natural |
:-. | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
:-: | Data.Type.Natural |
:<= | Data.Type.Natural |
@+ | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
@@ | Data.Type.Natural |
absurdOrd | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
Apply | Data.Type.Natural |
applySing | Data.Type.Natural |
boolToClassLeq | Data.Type.Natural |
boolToPropLeq | Data.Type.Natural |
cmpSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
cmpSuccStepR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
cmpZero | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
cmpZero' | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
coerceLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
coerceLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
Demote | Data.Type.Natural |
DemoteRep | Data.Type.Natural |
DiffNat | |
1 (Type/Class) | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
2 (Data Constructor) | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
Eight | Data.Type.Natural |
eight | Data.Type.Natural |
Eighteen | Data.Type.Natural |
eighteen | Data.Type.Natural |
EighteenSym0 | Data.Type.Natural |
EightSym0 | Data.Type.Natural |
Eleven | Data.Type.Natural |
eleven | Data.Type.Natural |
ElevenSym0 | Data.Type.Natural |
enumOrdinal | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
eqlCmpEQ | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
eqToRefl | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
Fifteen | Data.Type.Natural |
fifteen | Data.Type.Natural |
FifteenSym0 | Data.Type.Natural |
Five | Data.Type.Natural |
five | Data.Type.Natural |
FiveSym0 | Data.Type.Natural |
flipCompare | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
FlipOrdering | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
Four | Data.Type.Natural |
four | Data.Type.Natural |
FourSym0 | Data.Type.Natural |
Fourteen | Data.Type.Natural |
fourteen | Data.Type.Natural |
FourteenSym0 | Data.Type.Natural |
fromLeqView | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
FromPeano | Data.Type.Natural.Builtin |
fromPeanoInjective | Data.Type.Natural.Builtin |
fromPeanoMonotone | Data.Type.Natural.Builtin |
fromPeanoMultCong | Data.Type.Natural.Builtin |
fromPeanoOneCong | Data.Type.Natural.Builtin |
fromPeanoPlusCong | Data.Type.Natural.Builtin |
fromPeanoSuccCong | Data.Type.Natural.Builtin |
fromPeanoZeroCong | Data.Type.Natural.Builtin |
fromSing | Data.Type.Natural |
fromToPeano | Data.Type.Natural.Builtin |
geqToMax | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
geqToMin | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
gtToLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
HasOrdinal | Data.Type.Ordinal |
inclusion | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
inclusion' | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
induction | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
inductionNat | Data.Type.Natural.Builtin |
intToNat | Data.Type.Natural |
IsPeano | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
IsSucc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
IsZero | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
KindOf | Data.Type.Natural |
Leq | Data.Type.Natural |
leqAntisymm | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
LeqInstance | Data.Type.Natural |
leqNeqToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqNeqToSuccLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqRefl | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqReflexive | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqReversed | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqStep | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
LeqSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
leqSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqSucc' | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqSuccStepL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqSuccStepR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqToCmp | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqToGT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqToMax | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqToMin | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqTrans | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
LeqView | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
leqViewRefl | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqWitness | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
LeqZero | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
leqZero | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
leqZeroElim | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqReversed | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqRightPredSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqSuccLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqSuccStepL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqSuccStepR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqZero | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
lneqZeroAbsurd | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
ltRightPredSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
ltSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
ltSuccLToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
ltToLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
ltToLneq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
ltToNeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
ltToSuccLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
Max | Data.Type.Natural |
max | Data.Type.Natural |
maxComm | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
maxLeast | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
maxLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
maxLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
MaxSym0 | Data.Type.Natural |
MaxSym1 | Data.Type.Natural |
MaxSym2 | Data.Type.Natural |
maxZeroL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
maxZeroR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
Min | Data.Type.Natural |
min | Data.Type.Natural |
minComm | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
minLargest | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
minLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
minLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
minPlusTruncMinus | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
MinSym0 | Data.Type.Natural |
MinSym1 | Data.Type.Natural |
MinSym2 | Data.Type.Natural |
minusCong | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
minusCongL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
minusCongR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
minusNilpotent | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
minusPlus | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
minusSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
minusZero | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
minZeroL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
minZeroR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
mkOrdinalQQ | Data.Type.Ordinal |
mkSNatQQ | Data.Type.Natural.Class |
multAssoc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multComm | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multCong | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
multCongL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
multCongR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
multEqCancelL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multEqCancelR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multEqSuccElimL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multEqSuccElimR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multOneL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multOneR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multPlusDistrib | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multSuccL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multSuccR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multZeroL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
multZeroR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
N0 | Data.Type.Natural |
n0 | Data.Type.Natural |
N0Sym0 | Data.Type.Natural |
N1 | Data.Type.Natural |
n1 | Data.Type.Natural |
N10 | Data.Type.Natural |
n10 | Data.Type.Natural |
N10Sym0 | Data.Type.Natural |
N11 | Data.Type.Natural |
n11 | Data.Type.Natural |
N11Sym0 | Data.Type.Natural |
N12 | Data.Type.Natural |
n12 | Data.Type.Natural |
N12Sym0 | Data.Type.Natural |
N13 | Data.Type.Natural |
n13 | Data.Type.Natural |
N13Sym0 | Data.Type.Natural |
N14 | Data.Type.Natural |
n14 | Data.Type.Natural |
N14Sym0 | Data.Type.Natural |
N15 | Data.Type.Natural |
n15 | Data.Type.Natural |
N15Sym0 | Data.Type.Natural |
N16 | Data.Type.Natural |
n16 | Data.Type.Natural |
N16Sym0 | Data.Type.Natural |
N17 | Data.Type.Natural |
n17 | Data.Type.Natural |
N17Sym0 | Data.Type.Natural |
N18 | Data.Type.Natural |
n18 | Data.Type.Natural |
N18Sym0 | Data.Type.Natural |
N19 | Data.Type.Natural |
n19 | Data.Type.Natural |
N19Sym0 | Data.Type.Natural |
N1Sym0 | Data.Type.Natural |
N2 | Data.Type.Natural |
n2 | Data.Type.Natural |
N20 | Data.Type.Natural |
n20 | Data.Type.Natural |
N20Sym0 | Data.Type.Natural |
N2Sym0 | Data.Type.Natural |
N3 | Data.Type.Natural |
n3 | Data.Type.Natural |
N3Sym0 | Data.Type.Natural |
N4 | Data.Type.Natural |
n4 | Data.Type.Natural |
N4Sym0 | Data.Type.Natural |
N5 | Data.Type.Natural |
n5 | Data.Type.Natural |
N5Sym0 | Data.Type.Natural |
N6 | Data.Type.Natural |
n6 | Data.Type.Natural |
N6Sym0 | Data.Type.Natural |
N7 | Data.Type.Natural |
n7 | Data.Type.Natural |
N7Sym0 | Data.Type.Natural |
N8 | Data.Type.Natural |
n8 | Data.Type.Natural |
N8Sym0 | Data.Type.Natural |
N9 | Data.Type.Natural |
n9 | Data.Type.Natural |
N9Sym0 | Data.Type.Natural |
Nat | Data.Type.Natural |
natToInt | Data.Type.Natural |
Nine | Data.Type.Natural |
nine | Data.Type.Natural |
NineSym0 | Data.Type.Natural |
Nineteen | Data.Type.Natural |
nineteen | Data.Type.Natural |
NineteenSym0 | Data.Type.Natural |
nonSLeqToLT | Data.Type.Natural |
notLeqToLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
od | |
1 (Function) | Data.Type.Ordinal.Builtin |
2 (Function) | Data.Type.Ordinal.Peano |
odLit | Data.Type.Ordinal |
odPN | Data.Type.Ordinal |
OLt | |
1 (Data Constructor) | Data.Type.Ordinal |
2 (Data Constructor) | Data.Type.Ordinal.Builtin |
3 (Data Constructor) | Data.Type.Ordinal.Peano |
One | |
1 (Type/Class) | Data.Type.Natural |
2 (Type/Class) | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
one | Data.Type.Natural |
OneSym0 | Data.Type.Natural |
Ordinal | |
1 (Type/Class) | Data.Type.Ordinal |
2 (Type/Class) | Data.Type.Ordinal.Builtin |
3 (Type/Class) | Data.Type.Ordinal.Peano |
ordToInt | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
ordToSing | Data.Type.Ordinal |
OS | |
1 (Data Constructor) | Data.Type.Ordinal |
2 (Data Constructor) | Data.Type.Ordinal.Builtin |
3 (Data Constructor) | Data.Type.Ordinal.Peano |
OZ | |
1 (Data Constructor) | Data.Type.Ordinal |
2 (Data Constructor) | Data.Type.Ordinal.Builtin |
3 (Data Constructor) | Data.Type.Ordinal.Peano |
Peano | Data.Type.Natural.Builtin |
PeanoOrder | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusAssoc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusCancelLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusCancelLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusComm | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusCong | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
plusCongL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
plusCongR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural |
plusEqCancelL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusEqCancelR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusEqZeroL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusEqZeroR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusInjectiveL | Data.Type.Natural |
plusInjectiveR | Data.Type.Natural |
plusLeqL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusLeqR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusMinus | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusMinus' | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusMinusEqL | Data.Type.Natural |
plusMonotone | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusMonotoneL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusMonotoneR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusMultDistrib | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusNeutralL | Data.Type.Natural |
plusNeutralR | Data.Type.Natural |
plusStrictMonotone | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
plusSuccL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusSuccR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusZeroL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
plusZeroR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
predSucc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
predUnique | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
propToBoolLeq | Data.Type.Natural |
propToClassLeq | Data.Type.Natural |
Proxy | |
1 (Data Constructor) | Data.Type.Natural |
2 (Type/Class) | Data.Type.Natural |
reflToSEqual | Data.Type.Natural |
S | |
1 (Data Constructor) | Data.Type.Natural |
2 (Type/Class) | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
sEight | Data.Type.Natural |
sEighteen | Data.Type.Natural |
sEleven | Data.Type.Natural |
Seven | Data.Type.Natural |
seven | Data.Type.Natural |
SevenSym0 | Data.Type.Natural |
Seventeen | Data.Type.Natural |
seventeen | Data.Type.Natural |
SeventeenSym0 | Data.Type.Natural |
sFifteen | Data.Type.Natural |
sFive | Data.Type.Natural |
sFlipOrdering | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
sFour | Data.Type.Natural |
sFourteen | Data.Type.Natural |
sFromPeano | Data.Type.Natural.Builtin |
Sing | Data.Type.Natural |
sing | Data.Type.Natural |
singByProxy | Data.Type.Natural |
singByProxy# | Data.Type.Natural |
singFun1 | Data.Type.Natural |
singFun2 | Data.Type.Natural |
singFun3 | Data.Type.Natural |
singFun4 | Data.Type.Natural |
singFun5 | Data.Type.Natural |
singFun6 | Data.Type.Natural |
singFun7 | Data.Type.Natural |
singFun8 | Data.Type.Natural |
SingFunction1 | Data.Type.Natural |
SingFunction2 | Data.Type.Natural |
SingFunction3 | Data.Type.Natural |
SingFunction4 | Data.Type.Natural |
SingFunction5 | Data.Type.Natural |
SingFunction6 | Data.Type.Natural |
SingFunction7 | Data.Type.Natural |
SingFunction8 | Data.Type.Natural |
SingI | Data.Type.Natural |
SingInstance | |
1 (Data Constructor) | Data.Type.Natural |
2 (Type/Class) | Data.Type.Natural |
singInstance | Data.Type.Natural |
SingKind | Data.Type.Natural |
singThat | Data.Type.Natural |
Six | Data.Type.Natural |
six | Data.Type.Natural |
SixSym0 | Data.Type.Natural |
Sixteen | Data.Type.Natural |
sixteen | Data.Type.Natural |
SixteenSym0 | Data.Type.Natural |
SLambda | Data.Type.Natural |
sLeqCong | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
sLeqCongL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
sLeqCongR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
sLeqReflexive | Data.Type.Natural |
sMax | Data.Type.Natural |
sMin | Data.Type.Natural |
sN0 | Data.Type.Natural |
sN1 | Data.Type.Natural |
sN10 | Data.Type.Natural |
sN11 | Data.Type.Natural |
sN12 | Data.Type.Natural |
sN13 | Data.Type.Natural |
sN14 | Data.Type.Natural |
sN15 | Data.Type.Natural |
sN16 | Data.Type.Natural |
sN17 | Data.Type.Natural |
sN18 | Data.Type.Natural |
sN19 | Data.Type.Natural |
sN2 | Data.Type.Natural |
sN20 | Data.Type.Natural |
sN3 | Data.Type.Natural |
sN4 | Data.Type.Natural |
sN5 | Data.Type.Natural |
sN6 | Data.Type.Natural |
sN7 | Data.Type.Natural |
sN8 | Data.Type.Natural |
sN9 | Data.Type.Natural |
SNat | Data.Type.Natural |
snat | |
1 (Function) | Data.Type.Natural |
2 (Function) | Data.Type.Natural.Builtin |
sNatToInt | Data.Type.Natural |
sNatToOrd | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
sNatToOrd' | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
snEqZAbsurd | Data.Type.Natural |
sNine | Data.Type.Natural |
sNineteen | Data.Type.Natural |
SomeSing | |
1 (Data Constructor) | Data.Type.Natural |
2 (Type/Class) | Data.Type.Natural |
sOne | |
1 (Function) | Data.Type.Natural |
2 (Function) | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
sPred' | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
SS | Data.Type.Natural |
sSeven | Data.Type.Natural |
sSeventeen | Data.Type.Natural |
sSix | Data.Type.Natural |
sSixteen | Data.Type.Natural |
SSym0 | Data.Type.Natural |
SSym1 | Data.Type.Natural |
sTen | Data.Type.Natural |
sThirteen | Data.Type.Natural |
sThree | Data.Type.Natural |
sToPeano | Data.Type.Natural.Builtin |
sTwelve | Data.Type.Natural |
sTwenty | Data.Type.Natural |
sTwo | Data.Type.Natural |
Succ | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
succAndPlusOneL | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
succAndPlusOneR | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
succCong | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
succInj | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
succInj' | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
succLeqAbsurd | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
succLeqAbsurd' | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
SuccLeqSucc | Data.Type.Natural |
succLeqToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
succLeqZeroAbsurd | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
succLeqZeroAbsurd' | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
succLneqSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
succNonCyclic | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
succOneCong | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
succPred | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
SZ | Data.Type.Natural |
sZero | |
1 (Function) | Data.Type.Natural |
2 (Function) | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
Ten | Data.Type.Natural |
ten | Data.Type.Natural |
TenSym0 | Data.Type.Natural |
Thirteen | Data.Type.Natural |
thirteen | Data.Type.Natural |
ThirteenSym0 | Data.Type.Natural |
Three | Data.Type.Natural |
three | Data.Type.Natural |
ThreeSym0 | Data.Type.Natural |
toFromPeano | Data.Type.Natural.Builtin |
ToPeano | Data.Type.Natural.Builtin |
toPeanoInjective | Data.Type.Natural.Builtin |
toPeanoMonotone | Data.Type.Natural.Builtin |
toPeanoMultCong | Data.Type.Natural.Builtin |
toPeanoOneCong | Data.Type.Natural.Builtin |
toPeanoPlusCong | Data.Type.Natural.Builtin |
toPeanoSuccCong | Data.Type.Natural.Builtin |
toPeanoZeroCong | Data.Type.Natural.Builtin |
toSing | Data.Type.Natural |
truncMinusLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
Twelve | Data.Type.Natural |
twelve | Data.Type.Natural |
TwelveSym0 | Data.Type.Natural |
Twenty | Data.Type.Natural |
twenty | Data.Type.Natural |
TwentySym0 | Data.Type.Natural |
Two | Data.Type.Natural |
two | Data.Type.Natural |
TwoSym0 | Data.Type.Natural |
TyCon1 | Data.Type.Natural |
TyCon2 | Data.Type.Natural |
TyCon3 | Data.Type.Natural |
TyCon4 | Data.Type.Natural |
TyCon5 | Data.Type.Natural |
TyCon6 | Data.Type.Natural |
TyCon7 | Data.Type.Natural |
TyCon8 | Data.Type.Natural |
TyFun | Data.Type.Natural |
unsafeFromInt | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
unSingFun1 | Data.Type.Natural |
unSingFun2 | Data.Type.Natural |
unSingFun3 | Data.Type.Natural |
unSingFun4 | Data.Type.Natural |
unSingFun5 | Data.Type.Natural |
unSingFun6 | Data.Type.Natural |
unSingFun7 | Data.Type.Natural |
unSingFun8 | Data.Type.Natural |
vacuousOrd | |
1 (Function) | Data.Type.Ordinal |
2 (Function) | Data.Type.Ordinal.Builtin |
3 (Function) | Data.Type.Ordinal.Peano |
viewLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
withSing | Data.Type.Natural |
withSingI | Data.Type.Natural |
withSomeSing | Data.Type.Natural |
Z | Data.Type.Natural |
Zero | |
1 (Type/Class) | Data.Type.Natural |
2 (Type/Class) | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
3 (Data Constructor) | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
zero | Data.Type.Natural |
ZeroLeq | Data.Type.Natural |
zeroNoLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
ZeroOrSucc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class |
zeroOrSucc | Data.Type.Natural.Class.Arithmetic, Data.Type.Natural.Class, Data.Type.Natural, Data.Type.Natural.Builtin |
ZeroSym0 | Data.Type.Natural |
ZSym0 | Data.Type.Natural |
~> | Data.Type.Natural |