← Copula mathematical handbook

@[instance_reducible]

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.instLawfulUpwardEnumerableLTInt : LawfulUpwardEnumerableLT Int

@[instance_reducible]

instance Std.PRange.instHasSizeInt : Rxc.HasSize Int

Equations

• Std.PRange.instHasSizeInt = { size := fun (lo hi : Int) => (hi + 1 - lo).toNat }

instance Std.PRange.instLawfulHasSizeInt : Rxc.LawfulHasSize Int

instance Std.PRange.instIsAlwaysFiniteInt : Rxc.IsAlwaysFinite Int

@[instance_reducible]

instance Std.PRange.instHasSizeInt_1 : Rxo.HasSize Int

Equations

• Std.PRange.instHasSizeInt_1 = Std.Rxo.HasSize.ofClosed

instance Std.PRange.instLawfulHasSizeInt_1 : Rxo.LawfulHasSize Int

instance Std.PRange.instIsAlwaysFiniteInt_1 : Rxo.IsAlwaysFinite Int