Documentation

Init.Data.Range.Polymorphic.Nat

source
instance Std.PRange.instUpwardEnumerableNat :
UpwardEnumerable Nat
Equations
    source
    instance Std.PRange.instLeast?Nat :
    Least? Nat
    Equations
      source
      instance Std.PRange.instLawfulUpwardEnumerableLeast?Nat :
      LawfulUpwardEnumerableLeast? Nat
      source
      instance Std.PRange.instLawfulUpwardEnumerableLENat :
      LawfulUpwardEnumerableLE Nat
      source
      instance Std.PRange.instLawfulUpwardEnumerableNat :
      LawfulUpwardEnumerable Nat
      source
      instance Std.PRange.instLawfulUpwardEnumerableLTNat :
      LawfulUpwardEnumerableLT Nat
      source
      instance Std.PRange.instInfinitelyUpwardEnumerableNat :
      InfinitelyUpwardEnumerable Nat
      source
      instance Std.PRange.instHasSizeNat :
      Rxc.HasSize Nat
      Equations
        source
        instance Std.PRange.instHasSizeNat_1 :
        Rxo.HasSize Nat
        Equations
          source
          instance Std.PRange.instLawfulHasSizeNat :
          Rxc.LawfulHasSize Nat
          source
          instance Std.PRange.instIsAlwaysFiniteNat :
          Rxc.IsAlwaysFinite Nat
          source
          instance Std.PRange.instLawfulHasSizeNat_1 :
          Rxo.LawfulHasSize Nat
          source
          instance Std.PRange.instIsAlwaysFiniteNat_1 :
          Rxo.IsAlwaysFinite Nat
          source
          instance Std.PRange.instLinearlyUpwardEnumerableNat :
          LinearlyUpwardEnumerable Nat
          source
          instance Std.instHasRcoIntersectionNat :
          Roo.HasRcoIntersection Nat
          Equations
            source
            instance Std.instLawfulRcoIntersectionNat :
            Roo.LawfulRcoIntersection Nat
            source
            instance Std.instHasRcoIntersectionNat_1 :
            Roc.HasRcoIntersection Nat
            Equations
              source
              instance Std.instLawfulRcoIntersectionNat_1 :
              Roc.LawfulRcoIntersection Nat
              source
              instance Std.instHasRcoIntersectionNat_2 :
              Roi.HasRcoIntersection Nat
              Equations
                source
                instance Std.instLawfulRcoIntersectionNat_2 :
                Roi.LawfulRcoIntersection Nat
                source
                instance Std.instHasRcoIntersectionNat_3 :
                Rco.HasRcoIntersection Nat
                Equations
                  source
                  instance Std.instLawfulRcoIntersectionNat_3 :
                  Rco.LawfulRcoIntersection Nat
                  source
                  instance Std.instHasRcoIntersectionNat_4 :
                  Rcc.HasRcoIntersection Nat
                  Equations
                    source
                    instance Std.instLawfulRcoIntersectionNat_4 :
                    Rcc.LawfulRcoIntersection Nat
                    source
                    instance Std.instHasRcoIntersectionNat_5 :
                    Rci.HasRcoIntersection Nat
                    Equations
                      source
                      instance Std.instLawfulRcoIntersectionNat_5 :
                      Rci.LawfulRcoIntersection Nat
                      source
                      instance Std.instHasRcoIntersectionNat_6 :
                      Rio.HasRcoIntersection Nat
                      Equations
                        source
                        instance Std.instLawfulRcoIntersectionNat_6 :
                        Rio.LawfulRcoIntersection Nat
                        source
                        instance Std.instHasRcoIntersectionNat_7 :
                        Ric.HasRcoIntersection Nat
                        Equations
                          source
                          instance Std.instLawfulRcoIntersectionNat_7 :
                          Ric.LawfulRcoIntersection Nat