Documentation

Init.Data.Range.Polymorphic.Nat

@[instance_reducible]

instance Std.PRange.instUpwardEnumerableNat :

UpwardEnumerable Nat

@[instance_reducible]

instance Std.PRange.instLeast?Nat :

instance Std.PRange.instLawfulUpwardEnumerableLeast?Nat :

LawfulUpwardEnumerableLeast? Nat

instance Std.PRange.instLawfulUpwardEnumerableLENat :

LawfulUpwardEnumerableLE Nat

instance Std.PRange.instLawfulUpwardEnumerableNat :

LawfulUpwardEnumerable Nat

instance Std.PRange.instLawfulUpwardEnumerableLTNat :

LawfulUpwardEnumerableLT Nat

instance Std.PRange.instInfinitelyUpwardEnumerableNat :

InfinitelyUpwardEnumerable Nat

@[instance_reducible]

instance Std.PRange.instHasSizeNat :

Rxc.HasSize Nat

@[instance_reducible]

instance Std.PRange.instHasSizeNat_1 :

Rxo.HasSize Nat

instance Std.PRange.instLawfulHasSizeNat :

Rxc.LawfulHasSize Nat

instance Std.PRange.instIsAlwaysFiniteNat :

Rxc.IsAlwaysFinite Nat

instance Std.PRange.instLawfulHasSizeNat_1 :

Rxo.LawfulHasSize Nat

instance Std.PRange.instIsAlwaysFiniteNat_1 :

Rxo.IsAlwaysFinite Nat

instance Std.PRange.instLinearlyUpwardEnumerableNat :

LinearlyUpwardEnumerable Nat

The following instances are used for the implementation of array slices a.k.a. Subarray. See also Init.Data.Slice.Array.

@[instance_reducible]

instance Std.instHasRcoIntersectionNat :

Roo.HasRcoIntersection Nat

instance Std.instLawfulRcoIntersectionNat :

Roo.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_1 :

Roc.HasRcoIntersection Nat

instance Std.instLawfulRcoIntersectionNat_1 :

Roc.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_2 :

Roi.HasRcoIntersection Nat

instance Std.instLawfulRcoIntersectionNat_2 :

Roi.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_3 :

Rco.HasRcoIntersection Nat

instance Std.instLawfulRcoIntersectionNat_3 :

Rco.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_4 :

Rcc.HasRcoIntersection Nat

instance Std.instLawfulRcoIntersectionNat_4 :

Rcc.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_5 :

Rci.HasRcoIntersection Nat

instance Std.instLawfulRcoIntersectionNat_5 :

Rci.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_6 :

Rio.HasRcoIntersection Nat

instance Std.instLawfulRcoIntersectionNat_6 :

Rio.LawfulRcoIntersection Nat

@[instance_reducible]

instance Std.instHasRcoIntersectionNat_7 :

Ric.HasRcoIntersection Nat

instance Std.instLawfulRcoIntersectionNat_7 :

Ric.LawfulRcoIntersection Nat