S | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
SBool | Data.Type.Natural, Data.Type.Natural.Builtin |
sCmpNat | Data.Type.Natural, Data.Type.Natural.Builtin |
sCompare | Data.Type.Natural, Data.Type.Natural.Builtin |
sDiv | Data.Type.Natural, Data.Type.Natural.Builtin |
SEQ | Data.Type.Natural, Data.Type.Natural.Builtin |
SFalse | Data.Type.Natural, Data.Type.Natural.Builtin |
sFlipOrdering | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
SGT | Data.Type.Natural, Data.Type.Natural.Builtin |
sLeqCong | Data.Type.Natural.Lemma.Order |
sLeqCongL | Data.Type.Natural.Lemma.Order |
sLeqCongR | Data.Type.Natural.Lemma.Order |
sLog2 | Data.Type.Natural, Data.Type.Natural.Builtin |
SLT | Data.Type.Natural, Data.Type.Natural.Builtin |
sMax | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
sMin | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
sMod | Data.Type.Natural, Data.Type.Natural.Builtin |
SNat | Data.Type.Natural, Data.Type.Natural.Builtin |
sNat | Data.Type.Natural, Data.Type.Natural.Builtin |
snat | Data.Type.Natural, Data.Type.Natural.Builtin |
sNatP | Data.Type.Natural, Data.Type.Natural.Builtin |
sNatToOrd | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
sNatToOrd' | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
SomeNat | |
1 (Data Constructor) | Data.Type.Natural, Data.Type.Natural.Builtin |
2 (Type/Class) | Data.Type.Natural, Data.Type.Natural.Builtin |
someNatVal | Data.Type.Natural, Data.Type.Natural.Builtin |
SomeSNat | |
1 (Type/Class) | Data.Type.Natural, Data.Type.Natural.Builtin |
2 (Data Constructor) | Data.Type.Natural, Data.Type.Natural.Builtin |
sOne | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
SOrdering | Data.Type.Natural, Data.Type.Natural.Builtin |
sPred | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
sPred' | Data.Type.Natural.Lemma.Arithmetic |
sS | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
sSucc | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
STrue | Data.Type.Natural, Data.Type.Natural.Builtin |
Succ | |
1 (Type/Class) | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
2 (Data Constructor) | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
succAndPlusOneL | Data.Type.Natural.Lemma.Arithmetic |
succAndPlusOneR | Data.Type.Natural.Lemma.Arithmetic |
succCong | Data.Type.Natural.Lemma.Arithmetic |
succDiffNat | Data.Type.Natural.Lemma.Order |
succInj | Data.Type.Natural.Lemma.Arithmetic |
succInj' | Data.Type.Natural.Lemma.Arithmetic |
succLeqAbsurd | Data.Type.Natural.Lemma.Order |
succLeqAbsurd' | Data.Type.Natural.Lemma.Order |
SuccLeqSucc | Data.Type.Natural.Lemma.Order |
succLeqToLT | Data.Type.Natural.Lemma.Order |
succLeqZeroAbsurd | Data.Type.Natural.Lemma.Order |
succLeqZeroAbsurd' | Data.Type.Natural.Lemma.Order |
succLneqSucc | Data.Type.Natural.Lemma.Order |
succNonCyclic | Data.Type.Natural.Lemma.Arithmetic |
succOneCong | Data.Type.Natural.Lemma.Arithmetic |
succPred | Data.Type.Natural.Lemma.Arithmetic |
sZero | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |