Init.Data.Range.Polymorphic.Instances

This module provides instances that reduce the amount of code necessary to make a type compatible with the polymorphic ranges. For an example of the required work, take a look at Init.Data.Range.Polymorphic.Nat.

source

instance Std.PRange.instLawfulUpwardEnumerableLTOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulOrderLT {α : Type u_1} [LE α] [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulOrderLT α] :

LawfulUpwardEnumerableLT α

source

instance Std.PRange.instLawfulUpwardEnumerableLowerBoundClosedOfLawfulUpwardEnumerableLE {α : Type u_1} [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] :

LawfulUpwardEnumerableLowerBound BoundShape.closed α

source

instance Std.PRange.instLawfulUpwardEnumerableUpperBoundClosedOfLawfulUpwardEnumerableLEOfTransLe {α : Type u_1} [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2] :

LawfulUpwardEnumerableUpperBound BoundShape.closed α

source

instance Std.PRange.instLawfulUpwardEnumerableLowerBoundOpenOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLT {α : Type u_1} [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] :

LawfulUpwardEnumerableLowerBound BoundShape.open α

source

instance Std.PRange.instLawfulUpwardEnumerableUpperBoundOpenOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLT {α : Type u_1} [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] :

LawfulUpwardEnumerableUpperBound BoundShape.open α

source

instance Std.PRange.instLawfulUpwardEnumerableLowerBoundUnboundedOfLawfulUpwardEnumerableLeast? {α : Type u_1} [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] :

LawfulUpwardEnumerableLowerBound BoundShape.unbounded α

source

instance Std.PRange.instLinearlyUpwardEnumerableOfTotalLeOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLE {α : Type u_1} [LE α] [Total fun (x1 x2 : α) => x1 ≤ x2] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] :

LinearlyUpwardEnumerable α

source

instance Std.PRange.instLawfulUpwardEnumerableUpperBoundUnbounded {α : Type u_1} [UpwardEnumerable α] :

LawfulUpwardEnumerableUpperBound BoundShape.unbounded α

source

@[reducible, inline]

abbrev Std.PRange.RangeSize.openOfClosed {α : Type u_1} [RangeSize BoundShape.closed α] :

RangeSize BoundShape.open α

Creates a RangeSize .open α from a RangeSize .closed α instance. If the latter is lawful and certain other conditions hold, then the former is also lawful by LawfulRangeSize.open_of_closed.

Equations

Std.PRange.RangeSize.openOfClosed = { size := fun (bound : Std.PRange.Bound Std.PRange.BoundShape.open α) (a : α) => Std.PRange.RangeSize.size bound a - 1 }

Instances For

source

instance Std.PRange.LawfulRangeSize.open_of_closed {α : Type u_1} [UpwardEnumerable α] [LE α] [DecidableLE α] [LT α] [DecidableLT α] [LawfulOrderLT α] [IsPartialOrder α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [RangeSize BoundShape.closed α] [LawfulRangeSize BoundShape.closed α] :

LawfulRangeSize BoundShape.open α

source

instance Std.PRange.LawfulRangeSize.instHasFiniteRanges {α : Type u_1} {su : BoundShape} [UpwardEnumerable α] [LawfulUpwardEnumerable α] [RangeSize su α] [SupportsUpperBound su α] [LawfulRangeSize su α] :

HasFiniteRanges su α