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.instLawfulUpwardEnumerableLTOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulOrderLT {α : Type u_1} [LE α] [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [LawfulOrderLT α] :
PRange.LawfulUpwardEnumerableLT α
source
instance Std.instLinearlyUpwardEnumerableOfTotalLeOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLE {α : Type u_1} [LE α] [Total fun (x1 x2 : α) => x1 ≤ x2] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] :
PRange.LinearlyUpwardEnumerable α
source
instance Std.Rxc.instIsAlwaysFiniteOfLawfulHasSize {α : Type u_1} [LE α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [HasSize α] [LawfulHasSize α] :
IsAlwaysFinite α
source
@[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 }

Instances For

source
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 α
source
instance Std.Rxo.instIsAlwaysFiniteOfLawfulHasSize {α : Type u_1} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [HasSize α] [LawfulHasSize α] :
IsAlwaysFinite α
source
instance Std.Rxi.instIsAlwaysFiniteOfLawfulHasSize {α : Type u_1} [LT α] [PRange.UpwardEnumerable α] [PRange.LawfulUpwardEnumerable α] [HasSize α] [LawfulHasSize α] :
IsAlwaysFinite α