instance Std.PRange.instUpwardEnumerableNat : UpwardEnumerable Nat

Equations

• Std.PRange.instUpwardEnumerableNat = { succ? := fun (n : Nat) => some (n + 1), succMany? := fun (k n : Nat) => some (n + k) }

instance Std.PRange.instLeast?Nat : Least? Nat

Equations

• Std.PRange.instLeast?Nat = { least? := some 0 }

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.instLawfulUpwardEnumerableLowerBoundClosedNat : LawfulUpwardEnumerableLowerBound BoundShape.closed Nat

instance Std.PRange.instLawfulUpwardEnumerableUpperBoundClosedNat : LawfulUpwardEnumerableUpperBound BoundShape.closed Nat

instance Std.PRange.instLawfulUpwardEnumerableLowerBoundOpenNat : LawfulUpwardEnumerableLowerBound BoundShape.open Nat

instance Std.PRange.instLawfulUpwardEnumerableUpperBoundOpenNat : LawfulUpwardEnumerableUpperBound BoundShape.open Nat

instance Std.PRange.instLawfulUpwardEnumerableLowerBoundUnboundedNat : LawfulUpwardEnumerableLowerBound BoundShape.unbounded Nat

instance Std.PRange.instLawfulUpwardEnumerableUpperBoundUnboundedNat : LawfulUpwardEnumerableUpperBound BoundShape.unbounded Nat

instance Std.PRange.instInfinitelyUpwardEnumerableNat : InfinitelyUpwardEnumerable Nat

instance Std.PRange.instRangeSizeClosedNat : RangeSize BoundShape.closed Nat

Equations

• Std.PRange.instRangeSizeClosedNat = { size := fun (bound : Std.PRange.Bound Std.PRange.BoundShape.closed Nat) (a : Nat) => bound + 1 - a }

instance Std.PRange.instRangeSizeOpenNat : RangeSize BoundShape.open Nat

Equations

• Std.PRange.instRangeSizeOpenNat = Std.PRange.RangeSize.openOfClosed

instance Std.PRange.instLawfulRangeSizeClosedNat : LawfulRangeSize BoundShape.closed Nat

instance Std.PRange.instLawfulRangeSizeOpenNat : LawfulRangeSize BoundShape.open Nat

instance Std.PRange.instHasFiniteRangesClosedNat : HasFiniteRanges BoundShape.closed Nat

instance Std.PRange.instHasFiniteRangesOpenNat : HasFiniteRanges BoundShape.open 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 Std.PRange.instClosedOpenIntersectionMkOpenNat : ClosedOpenIntersection { lower := BoundShape.open, upper := BoundShape.open } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkOpenNat : LawfulClosedOpenIntersection { lower := BoundShape.open, upper := BoundShape.open } Nat

instance Std.PRange.instClosedOpenIntersectionMkOpenClosedNat : ClosedOpenIntersection { lower := BoundShape.open, upper := BoundShape.closed } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkOpenClosedNat : LawfulClosedOpenIntersection { lower := BoundShape.open, upper := BoundShape.closed } Nat

instance Std.PRange.instClosedOpenIntersectionMkOpenUnboundedNat : ClosedOpenIntersection { lower := BoundShape.open, upper := BoundShape.unbounded } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkOpenUnboundedNat : LawfulClosedOpenIntersection { lower := BoundShape.open, upper := BoundShape.unbounded } Nat

instance Std.PRange.instClosedOpenIntersectionMkClosedOpenNat : ClosedOpenIntersection { lower := BoundShape.closed, upper := BoundShape.open } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkClosedOpenNat : LawfulClosedOpenIntersection { lower := BoundShape.closed, upper := BoundShape.open } Nat

instance Std.PRange.instClosedOpenIntersectionMkClosedNat : ClosedOpenIntersection { lower := BoundShape.closed, upper := BoundShape.closed } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkClosedNat : LawfulClosedOpenIntersection { lower := BoundShape.closed, upper := BoundShape.closed } Nat

instance Std.PRange.instClosedOpenIntersectionMkClosedUnboundedNat : ClosedOpenIntersection { lower := BoundShape.closed, upper := BoundShape.unbounded } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkClosedUnboundedNat : LawfulClosedOpenIntersection { lower := BoundShape.closed, upper := BoundShape.unbounded } Nat

instance Std.PRange.instClosedOpenIntersectionMkUnboundedOpenNat : ClosedOpenIntersection { lower := BoundShape.unbounded, upper := BoundShape.open } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkUnboundedOpenNat : LawfulClosedOpenIntersection { lower := BoundShape.unbounded, upper := BoundShape.open } Nat

instance Std.PRange.instClosedOpenIntersectionMkUnboundedClosedNat : ClosedOpenIntersection { lower := BoundShape.unbounded, upper := BoundShape.closed } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkUnboundedClosedNat : LawfulClosedOpenIntersection { lower := BoundShape.unbounded, upper := BoundShape.closed } Nat

instance Std.PRange.instClosedOpenIntersectionMkUnboundedNat : ClosedOpenIntersection { lower := BoundShape.unbounded, upper := BoundShape.unbounded } Nat

Equations

• One or more equations did not get rendered due to their size.

instance Std.PRange.instLawfulClosedOpenIntersectionMkUnboundedNat : LawfulClosedOpenIntersection { lower := BoundShape.unbounded, upper := BoundShape.unbounded } Nat