| %* | Data.Type.Natural, Data.Type.Natural.Builtin |
| %+ | Data.Type.Natural, Data.Type.Natural.Builtin |
| %- | Data.Type.Natural, Data.Type.Natural.Builtin |
| %-. | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| %<=? | Data.Type.Natural, Data.Type.Natural.Builtin |
| %<? | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| %>=? | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| %>? | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| %^ | Data.Type.Natural, Data.Type.Natural.Builtin |
| %~ | Data.Type.Natural, Data.Type.Natural.Builtin |
| * | Data.Type.Natural, Data.Type.Natural.Builtin |
| + | Data.Type.Natural, Data.Type.Natural.Builtin |
| - | Data.Type.Natural, Data.Type.Natural.Builtin |
| -. | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| :<: | Data.Type.Natural.Lemma.Order |
| < | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| <= | Data.Type.Natural, Data.Type.Natural.Builtin |
| <=? | Data.Type.Natural, Data.Type.Natural.Builtin |
| <? | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| === | Data.Type.Natural, Data.Type.Natural.Builtin |
| > | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| >= | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| >=? | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| >? | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| @+ | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| absurdOrd | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| boolToPropLeq | Data.Type.Natural.Lemma.Order |
| boolToPropLt | Data.Type.Natural.Lemma.Order |
| CmpNat | Data.Type.Natural, Data.Type.Natural.Builtin |
| cmpSucc | Data.Type.Natural.Lemma.Order |
| cmpSuccStepR | Data.Type.Natural.Lemma.Order |
| cmpZero | Data.Type.Natural.Lemma.Order |
| cmpZero' | Data.Type.Natural.Lemma.Order |
| coerceLeqL | Data.Type.Natural.Lemma.Order |
| coerceLeqR | Data.Type.Natural.Lemma.Order |
| compareCongR | Data.Type.Natural.Lemma.Order |
| congFlipOrdering | Data.Type.Natural.Lemma.Order |
| DiffNat | |
| 1 (Type/Class) | Data.Type.Natural.Lemma.Order |
| 2 (Data Constructor) | Data.Type.Natural.Lemma.Order |
| Div | Data.Type.Natural, Data.Type.Natural.Builtin |
| enumOrdinal | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| eqlCmpEQ | Data.Type.Natural.Lemma.Order |
| eqToRefl | Data.Type.Natural.Lemma.Order |
| Equal | Data.Type.Natural, Data.Type.Natural.Builtin |
| Equality | Data.Type.Natural, Data.Type.Natural.Builtin |
| flipCmpNat | Data.Type.Natural.Lemma.Order |
| FlipOrdering | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| fromLeqView | Data.Type.Natural.Lemma.Order |
| geqToMax | Data.Type.Natural.Lemma.Order |
| geqToMin | Data.Type.Natural.Lemma.Order |
| gtToLeq | Data.Type.Natural.Lemma.Order |
| inclusion | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| inclusion' | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| induction | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| IsSucc | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| IsZero | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| KnownNat | Data.Type.Natural, Data.Type.Natural.Builtin |
| Leq | Data.Type.Natural.Lemma.Order |
| leqAntisymm | Data.Type.Natural.Lemma.Order |
| leqLhs | Data.Type.Natural.Lemma.Order |
| leqNeqToLT | Data.Type.Natural.Lemma.Order |
| leqNeqToSuccLeq | Data.Type.Natural.Lemma.Order |
| leqRefl | Data.Type.Natural.Lemma.Order |
| leqReflexive | Data.Type.Natural.Lemma.Order |
| leqRhs | Data.Type.Natural.Lemma.Order |
| leqStep | Data.Type.Natural.Lemma.Order |
| LeqSucc | Data.Type.Natural.Lemma.Order |
| leqSucc | Data.Type.Natural.Lemma.Order |
| leqSucc' | Data.Type.Natural.Lemma.Order |
| leqSuccStepL | Data.Type.Natural.Lemma.Order |
| leqSuccStepR | Data.Type.Natural.Lemma.Order |
| leqToCmp | Data.Type.Natural.Lemma.Order |
| leqToGT | Data.Type.Natural.Lemma.Order |
| leqToLT | Data.Type.Natural.Lemma.Order |
| leqToMax | Data.Type.Natural.Lemma.Order |
| leqToMin | Data.Type.Natural.Lemma.Order |
| leqTrans | Data.Type.Natural.Lemma.Order |
| LeqView | Data.Type.Natural.Lemma.Order |
| leqViewRefl | Data.Type.Natural.Lemma.Order |
| LeqWitness | Data.Type.Natural.Lemma.Order |
| leqWitness | Data.Type.Natural.Lemma.Order |
| LeqZero | Data.Type.Natural.Lemma.Order |
| leqZero | Data.Type.Natural.Lemma.Order |
| leqZeroElim | Data.Type.Natural.Lemma.Order |
| lneqReversed | Data.Type.Natural.Lemma.Order |
| lneqRightPredSucc | Data.Type.Natural.Lemma.Order |
| lneqSucc | Data.Type.Natural.Lemma.Order |
| lneqSuccLeq | Data.Type.Natural.Lemma.Order |
| lneqSuccStepL | Data.Type.Natural.Lemma.Order |
| lneqSuccStepR | Data.Type.Natural.Lemma.Order |
| lneqToLT | Data.Type.Natural.Lemma.Order |
| lneqZero | Data.Type.Natural.Lemma.Order |
| lneqZeroAbsurd | Data.Type.Natural.Lemma.Order |
| Log2 | Data.Type.Natural, Data.Type.Natural.Builtin |
| ltRightPredSucc | Data.Type.Natural.Lemma.Order |
| ltSucc | Data.Type.Natural.Lemma.Order |
| ltSuccLToLT | Data.Type.Natural.Lemma.Order |
| ltToLeq | Data.Type.Natural.Lemma.Order |
| ltToLneq | Data.Type.Natural.Lemma.Order |
| ltToNeq | Data.Type.Natural.Lemma.Order |
| ltToSuccLeq | Data.Type.Natural.Lemma.Order |
| Max | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| maxComm | Data.Type.Natural.Lemma.Order |
| maxLeast | Data.Type.Natural.Lemma.Order |
| maxLeqL | Data.Type.Natural.Lemma.Order |
| maxLeqR | Data.Type.Natural.Lemma.Order |
| maxZeroL | Data.Type.Natural.Lemma.Order |
| maxZeroR | Data.Type.Natural.Lemma.Order |
| Min | Data.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin |
| minComm | Data.Type.Natural.Lemma.Order |
| minLargest | Data.Type.Natural.Lemma.Order |
| minLeqL | Data.Type.Natural.Lemma.Order |
| minLeqR | Data.Type.Natural.Lemma.Order |
| minPlusTruncMinus | Data.Type.Natural.Lemma.Order |
| minusCong | Data.Type.Natural.Lemma.Arithmetic |
| minusCongL | Data.Type.Natural.Lemma.Arithmetic |
| minusCongR | Data.Type.Natural.Lemma.Arithmetic |
| minusNilpotent | Data.Type.Natural.Lemma.Arithmetic |
| minusPlus | Data.Type.Natural.Lemma.Order |
| minusSucc | Data.Type.Natural.Lemma.Order |
| minusZero | Data.Type.Natural.Lemma.Arithmetic |
| minZeroL | Data.Type.Natural.Lemma.Order |
| minZeroR | Data.Type.Natural.Lemma.Order |
| Mod | Data.Type.Natural, Data.Type.Natural.Builtin |
| multAssoc | Data.Type.Natural.Lemma.Arithmetic |
| multComm | Data.Type.Natural.Lemma.Arithmetic |
| multCong | Data.Type.Natural.Lemma.Arithmetic |
| multCongL | Data.Type.Natural.Lemma.Arithmetic |
| multCongR | Data.Type.Natural.Lemma.Arithmetic |
| multEqCancelL | Data.Type.Natural.Lemma.Arithmetic |
| multEqCancelR | Data.Type.Natural.Lemma.Arithmetic |
| multEqSuccElimL | Data.Type.Natural.Lemma.Arithmetic |
| multEqSuccElimR | Data.Type.Natural.Lemma.Arithmetic |
| multOneL | Data.Type.Natural.Lemma.Arithmetic |
| multOneR | Data.Type.Natural.Lemma.Arithmetic |
| multPlusDistrib | Data.Type.Natural.Lemma.Arithmetic |
| multSuccL | Data.Type.Natural.Lemma.Arithmetic |
| multSuccL' | Data.Type.Natural.Lemma.Arithmetic |
| multSuccR | Data.Type.Natural.Lemma.Arithmetic |
| multZeroL | Data.Type.Natural.Lemma.Arithmetic |
| multZeroR | Data.Type.Natural.Lemma.Arithmetic |
| Nat | Data.Type.Natural, Data.Type.Natural.Builtin |
| naturalToOrd | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| naturalToOrd' | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| natVal | Data.Type.Natural, Data.Type.Natural.Builtin |
| natVal' | Data.Type.Natural, Data.Type.Natural.Builtin |
| NonEqual | Data.Type.Natural, Data.Type.Natural.Builtin |
| notLeqToLeq | Data.Type.Natural.Lemma.Order |
| od | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| OLt | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| One | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| Ordinal | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| ordToNatural | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| ordToSNat | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| OS | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| OZ | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| plugin | Data.Type.Natural.Presburger.MinMaxSolver |
| plusAssoc | Data.Type.Natural.Lemma.Arithmetic |
| plusCancelLeqL | Data.Type.Natural.Lemma.Order |
| plusCancelLeqR | Data.Type.Natural.Lemma.Order |
| plusComm | Data.Type.Natural.Lemma.Arithmetic |
| plusCong | Data.Type.Natural.Lemma.Arithmetic |
| plusCongL | Data.Type.Natural.Lemma.Arithmetic |
| plusCongR | Data.Type.Natural.Lemma.Arithmetic |
| plusEqCancelL | Data.Type.Natural.Lemma.Arithmetic |
| plusEqCancelR | Data.Type.Natural.Lemma.Arithmetic |
| plusEqZeroL | Data.Type.Natural.Lemma.Arithmetic |
| plusEqZeroR | Data.Type.Natural.Lemma.Arithmetic |
| plusLeqL | Data.Type.Natural.Lemma.Order |
| plusLeqR | Data.Type.Natural.Lemma.Order |
| plusMinus | Data.Type.Natural.Lemma.Arithmetic |
| plusMinus' | Data.Type.Natural.Lemma.Arithmetic |
| plusMonotone | Data.Type.Natural.Lemma.Order |
| plusMonotoneL | Data.Type.Natural.Lemma.Order |
| plusMonotoneR | Data.Type.Natural.Lemma.Order |
| plusMultDistrib | Data.Type.Natural.Lemma.Arithmetic |
| plusStrictMonotone | Data.Type.Natural.Lemma.Order |
| plusSuccL | Data.Type.Natural.Lemma.Arithmetic |
| plusSuccR | Data.Type.Natural.Lemma.Arithmetic |
| plusZeroL | Data.Type.Natural.Lemma.Arithmetic |
| plusZeroR | Data.Type.Natural.Lemma.Arithmetic |
| Pred | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| predCong | Data.Type.Natural.Lemma.Arithmetic |
| predSucc | Data.Type.Natural.Lemma.Arithmetic |
| predUnique | Data.Type.Natural.Lemma.Arithmetic |
| propToBoolLeq | Data.Type.Natural.Lemma.Order |
| propToBoolLt | Data.Type.Natural.Lemma.Order |
| reallyUnsafeNaturalToOrd | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| 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 |
| toNatural | Data.Type.Natural, Data.Type.Natural.Builtin |
| toSomeSNat | Data.Type.Natural, Data.Type.Natural.Builtin |
| truncMinusLeq | Data.Type.Natural.Lemma.Order |
| unsafeNaturalToOrd | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| unsafeNaturalToOrd' | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| vacuousOrd | Data.Type.Ordinal, Data.Type.Ordinal.Builtin |
| viewLeq | Data.Type.Natural.Lemma.Order |
| viewNat | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| withKnownNat | Data.Type.Natural, Data.Type.Natural.Builtin |
| withSNat | Data.Type.Natural, Data.Type.Natural.Builtin |
| Zero | |
| 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 |
| ZeroLeq | Data.Type.Natural.Lemma.Order |
| zeroNoLT | Data.Type.Natural.Lemma.Order |
| ZeroOrSucc | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| zeroOrSucc | Data.Type.Natural.Lemma.Arithmetic, Data.Type.Natural, Data.Type.Natural.Builtin |
| ^ | Data.Type.Natural, Data.Type.Natural.Builtin |