source
instance Std.PRange.instUpwardEnumerableNat :
UpwardEnumerable Nat
Equations

- Std.PRange.instUpwardEnumerableNat = { succ? := fun (n : Nat) => some (n + 1), succMany? := fun (k n : Nat) => some (n + k) }

source
instance Std.PRange.instLeast?Nat :
Least? Nat
Equations

- Std.PRange.instLeast?Nat = { least? := some 0 }

source
instance Std.PRange.instLawfulUpwardEnumerableLeast?Nat :
LawfulUpwardEnumerableLeast? Nat
source
instance Std.PRange.instLawfulUpwardEnumerableLENat :
LawfulUpwardEnumerableLE Nat
source
instance Std.PRange.instLawfulUpwardEnumerableNat :
LawfulUpwardEnumerable Nat
source
instance Std.PRange.instLawfulUpwardEnumerableLTNat :
LawfulUpwardEnumerableLT Nat
source
instance Std.PRange.instInfinitelyUpwardEnumerableNat :
InfinitelyUpwardEnumerable Nat
source
instance Std.PRange.instHasSizeNat :
Rxc.HasSize Nat
Equations

- Std.PRange.instHasSizeNat = { size := fun (lo hi : Nat) => hi + 1 - lo }

source
instance Std.PRange.instHasSizeNat_1 :
Rxo.HasSize Nat
Equations

- Std.PRange.instHasSizeNat_1 = Std.Rxo.HasSize.ofClosed

source
instance Std.PRange.instLawfulHasSizeNat :
Rxc.LawfulHasSize Nat
source
instance Std.PRange.instIsAlwaysFiniteNat :
Rxc.IsAlwaysFinite Nat
source
instance Std.PRange.instLawfulHasSizeNat_1 :
Rxo.LawfulHasSize Nat
source
instance Std.PRange.instIsAlwaysFiniteNat_1 :
Rxo.IsAlwaysFinite Nat
source
instance Std.PRange.instLinearlyUpwardEnumerableNat :
LinearlyUpwardEnumerable Nat
source
instance Std.instHasRcoIntersectionNat :
Roo.HasRcoIntersection Nat
Equations

- Std.instHasRcoIntersectionNat = { intersection := fun (r : Std.Roo Nat) (s : Std.Rco Nat) => (max (r.lower + 1) s.lower)...min r.upper s.upper }

source
instance Std.instLawfulRcoIntersectionNat :
Roo.LawfulRcoIntersection Nat
source
instance Std.instHasRcoIntersectionNat_1 :
Roc.HasRcoIntersection Nat
Equations

- Std.instHasRcoIntersectionNat_1 = { intersection := fun (r : Std.Roc Nat) (s : Std.Rco Nat) => (max (r.lower + 1) s.lower)...min (r.upper + 1) s.upper }

source
instance Std.instLawfulRcoIntersectionNat_1 :
Roc.LawfulRcoIntersection Nat
source
instance Std.instHasRcoIntersectionNat_2 :
Roi.HasRcoIntersection Nat
Equations

- Std.instHasRcoIntersectionNat_2 = { intersection := fun (r : Std.Roi Nat) (s : Std.Rco Nat) => (max (r.lower + 1) s.lower)...s.upper }

source
instance Std.instLawfulRcoIntersectionNat_2 :
Roi.LawfulRcoIntersection Nat
source
instance Std.instHasRcoIntersectionNat_3 :
Rco.HasRcoIntersection Nat
Equations

- Std.instHasRcoIntersectionNat_3 = { intersection := fun (r s : Std.Rco Nat) => (max r.lower s.lower)...min r.upper s.upper }

source
instance Std.instLawfulRcoIntersectionNat_3 :
Rco.LawfulRcoIntersection Nat
source
instance Std.instHasRcoIntersectionNat_4 :
Rcc.HasRcoIntersection Nat
Equations

- Std.instHasRcoIntersectionNat_4 = { intersection := fun (r : Std.Rcc Nat) (s : Std.Rco Nat) => (max r.lower s.lower)...min (r.upper + 1) s.upper }

source
instance Std.instLawfulRcoIntersectionNat_4 :
Rcc.LawfulRcoIntersection Nat
source
instance Std.instHasRcoIntersectionNat_5 :
Rci.HasRcoIntersection Nat
Equations

- Std.instHasRcoIntersectionNat_5 = { intersection := fun (r : Std.Rci Nat) (s : Std.Rco Nat) => (max r.lower s.lower)...s.upper }

source
instance Std.instLawfulRcoIntersectionNat_5 :
Rci.LawfulRcoIntersection Nat
source
instance Std.instHasRcoIntersectionNat_6 :
Rio.HasRcoIntersection Nat
Equations

- Std.instHasRcoIntersectionNat_6 = { intersection := fun (r : Std.Rio Nat) (s : Std.Rco Nat) => s.lower...min r.upper s.upper }

source
instance Std.instLawfulRcoIntersectionNat_6 :
Rio.LawfulRcoIntersection Nat
source
instance Std.instHasRcoIntersectionNat_7 :
Ric.HasRcoIntersection Nat
Equations

- Std.instHasRcoIntersectionNat_7 = { intersection := fun (r : Std.Ric Nat) (s : Std.Rco Nat) => s.lower...min (r.upper + 1) s.upper }

source
instance Std.instLawfulRcoIntersectionNat_7 :
Ric.LawfulRcoIntersection Nat