instance Std.PRange.instUpwardEnumerableInt : UpwardEnumerable Int

Equations

• Std.PRange.instUpwardEnumerableInt = { succ? := fun (x : Int) => some (x + 1), succMany? := fun (n : Nat) (x : Int) => some (x + ↑n) }

instance Std.PRange.instLawfulUpwardEnumerableInt : LawfulUpwardEnumerable Int

instance Std.PRange.instInfinitelyUpwardEnumerableInt : InfinitelyUpwardEnumerable Int

instance Std.PRange.instLawfulUpwardEnumerableLEInt : LawfulUpwardEnumerableLE Int

instance Std.PRange.instLawfulOrderLTInt : LawfulOrderLT Int

instance Std.PRange.instLawfulUpwardEnumerableLTInt : LawfulUpwardEnumerableLT Int

instance Std.PRange.instLawfulUpwardEnumerableLTInt_1 : LawfulUpwardEnumerableLT Int

instance Std.PRange.instLawfulUpwardEnumerableLowerBoundClosedInt : LawfulUpwardEnumerableLowerBound BoundShape.closed Int

instance Std.PRange.instLawfulUpwardEnumerableUpperBoundClosedInt : LawfulUpwardEnumerableUpperBound BoundShape.closed Int

instance Std.PRange.instLawfulUpwardEnumerableLowerBoundOpenInt : LawfulUpwardEnumerableLowerBound BoundShape.open Int

instance Std.PRange.instLawfulUpwardEnumerableUpperBoundOpenInt : LawfulUpwardEnumerableUpperBound BoundShape.open Int

instance Std.PRange.instRangeSizeClosedInt : RangeSize BoundShape.closed Int

Equations

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

instance Std.PRange.instRangeSizeOpenInt : RangeSize BoundShape.open Int

Equations

• Std.PRange.instRangeSizeOpenInt = Std.PRange.RangeSize.openOfClosed

instance Std.PRange.instLawfulRangeSizeClosedInt : LawfulRangeSize BoundShape.closed Int