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.

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

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

instance Std.Rxc.instIsAlwaysFiniteOfLawfulHasSize {α : Type u_1} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [HasSize α] [LawfulHasSize α] : IsAlwaysFinite α

@[reducible, inline]

abbrev Std.Rxo.HasSize.ofClosed {α : Type u_1} [Rxc.HasSize α] : HasSize α

Creates a HasSize α from a HasSize α instance. If the latter is lawful and certain other conditions hold, then the former is also lawful by Rxo.LawfulHasSize.of_closed.

Equations

• Std.Rxo.HasSize.ofClosed = { size := fun (lo hi : α) => Std.Rxc.HasSize.size lo hi - 1 }

instance Std.Rxo.LawfulHasSize.of_closed {α : Type u_1} [PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [LT α] [DecidableLT α] [LawfulOrderLT α] [IsPartialOrder α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] : LawfulHasSize α

instance Std.Rxo.instIsAlwaysFiniteOfLawfulHasSize {α : Type u_1} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [HasSize α] [LawfulHasSize α] : IsAlwaysFinite α

instance Std.Rxi.instIsAlwaysFiniteOfLawfulHasSize {α : Type u_1} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [HasSize α] [LawfulHasSize α] : IsAlwaysFinite α