type-natural-1.0.0.0: Type-level natural and proofs of their properties.

Index - M

MaxData.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin
maxCommData.Type.Natural.Lemma.Order
maxLeastData.Type.Natural.Lemma.Order
maxLeqLData.Type.Natural.Lemma.Order
maxLeqRData.Type.Natural.Lemma.Order
maxZeroLData.Type.Natural.Lemma.Order
maxZeroRData.Type.Natural.Lemma.Order
MinData.Type.Natural.Lemma.Order, Data.Type.Natural, Data.Type.Natural.Builtin
minCommData.Type.Natural.Lemma.Order
minLargestData.Type.Natural.Lemma.Order
minLeqLData.Type.Natural.Lemma.Order
minLeqRData.Type.Natural.Lemma.Order
minPlusTruncMinusData.Type.Natural.Lemma.Order
minusCongData.Type.Natural.Lemma.Arithmetic
minusCongLData.Type.Natural.Lemma.Arithmetic
minusCongRData.Type.Natural.Lemma.Arithmetic
minusNilpotentData.Type.Natural.Lemma.Arithmetic
minusPlusData.Type.Natural.Lemma.Order
minusSuccData.Type.Natural.Lemma.Order
minusZeroData.Type.Natural.Lemma.Arithmetic
minZeroLData.Type.Natural.Lemma.Order
minZeroRData.Type.Natural.Lemma.Order
ModData.Type.Natural, Data.Type.Natural.Builtin
multAssocData.Type.Natural.Lemma.Arithmetic
multCommData.Type.Natural.Lemma.Arithmetic
multCongData.Type.Natural.Lemma.Arithmetic
multCongLData.Type.Natural.Lemma.Arithmetic
multCongRData.Type.Natural.Lemma.Arithmetic
multEqCancelLData.Type.Natural.Lemma.Arithmetic
multEqCancelRData.Type.Natural.Lemma.Arithmetic
multEqSuccElimLData.Type.Natural.Lemma.Arithmetic
multEqSuccElimRData.Type.Natural.Lemma.Arithmetic
multOneLData.Type.Natural.Lemma.Arithmetic
multOneRData.Type.Natural.Lemma.Arithmetic
multPlusDistribData.Type.Natural.Lemma.Arithmetic
multSuccLData.Type.Natural.Lemma.Arithmetic
multSuccL'Data.Type.Natural.Lemma.Arithmetic
multSuccRData.Type.Natural.Lemma.Arithmetic
multZeroLData.Type.Natural.Lemma.Arithmetic
multZeroRData.Type.Natural.Lemma.Arithmetic