Documentation

Init.Data.Range.Polymorphic.Nat

instance Std.PRange.instUpwardEnumerableNat :

UpwardEnumerable Nat

Equations

instance Std.PRange.instLeast?Nat :

Equations

instance Std.PRange.instLawfulUpwardEnumerableLENat :

LawfulUpwardEnumerableLE Nat

instance Std.PRange.instLawfulUpwardEnumerableLTNat :

LawfulUpwardEnumerableLT Nat

instance Std.PRange.instLawfulUpwardEnumerableNat :

LawfulUpwardEnumerable 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.instLinearlyUpwardEnumerableNat :

LinearlyUpwardEnumerable Nat

instance Std.PRange.instInfinitelyUpwardEnumerableNat :

InfinitelyUpwardEnumerable Nat

instance Std.PRange.instHasFiniteRangesClosedNat :

HasFiniteRanges BoundShape.closed Nat

instance Std.PRange.instHasFiniteRangesOpenNat :

HasFiniteRanges BoundShape.open Nat

instance Std.PRange.instRangeSizeClosedNat :

RangeSize BoundShape.closed Nat

Equations

instance Std.PRange.instRangeSizeOpenNat :

RangeSize BoundShape.open Nat

Equations

instance Std.PRange.instLawfulRangeSizeClosedNat :

LawfulRangeSize BoundShape.closed Nat

instance Std.PRange.instLawfulRangeSizeOpenNat :

LawfulRangeSize BoundShape.open Nat

instance Std.PRange.instClosedOpenIntersectionMkOpenNat :

ClosedOpenIntersection { lower := BoundShape.open, upper := BoundShape.open } Nat

Equations

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

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

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

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

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

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

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

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

instance Std.PRange.instLawfulClosedOpenIntersectionMkUnboundedNat :

LawfulClosedOpenIntersection { lower := BoundShape.unbounded, upper := BoundShape.unbounded } Nat