source
structure Std.Rcc (α : Type u) :
Type u

A range of elements of `α` with closed lower and upper bounds.

`a...=b` is the range of all values greater than or equal to `a : α` and less than or equal to `b : α`. This is notation for `Rcc.mk a b`.

- lower : α
- upper : α

Instances For

source
structure Std.Rco (α : Type u) :
Type u

A range of elements of `α` with a closed lower bound and an open upper bound.

`a...b` or `a...<b` is the range of all values greater than or equal to `a : α` and less than `b : α`. This is notation for `Rco.mk a b`.

- lower : α
- upper : α

Instances For

source
structure Std.Rci (α : Type u) :
Type u

An upward-unbounded range of elements of `α` with a closed lower bound.

`a...*` is the range of all values greater than or equal to `a : α`. This is notation for `Rci.mk a`.

- lower : α

Instances For

source
structure Std.Roc (α : Type u) :
Type u

A range of elements of `α` with an open lower bound and a closed upper bound.

`a<...=b` is the range of all values greater than `a : α` and less than or equal to `b : α`. This is notation for `Roc.mk a b`.

- lower : α
- upper : α

Instances For

source
structure Std.Roo (α : Type u) :
Type u

A range of elements of `α` with an open lower and upper bounds.

`a<...b` or `a<...<b` is the range of all values greater than `a : α` and less than `b : α`. This is notation for `Roo.mk a b`.

- lower : α
- upper : α

Instances For

source
structure Std.Roi (α : Type u) :
Type u

An upward-unbounded range of elements of `α` with an open lower bound.

`a<...*` is the range of all values greater than `a : α`. This is notation for `Roi.mk a`.

- lower : α

Instances For

source
structure Std.Ric (α : Type u) :
Type u

A downward-unbounded range of elements of `α` with a closed upper bound.

`*...=b` is the range of all values less than or equal to `b : α`. This is notation for `Ric.mk b`.

- upper : α

Instances For

source
structure Std.Rio (α : Type u) :
Type u

A downward-unbounded range of elements of `α` with an open upper bound.

`*...b` or `*...<b` is the range of all values less than `b : α`. This is notation for `Rio.mk b`.

- upper : α

Instances For

source
structure Std.Rii (α : Type u) :
Type

A full range of all elements of `α`. Its only inhabitant is the range `*...*`, which is notation for `Rii.mk`.

Instances For

source
def Std.«term_...*» :
Lean.TrailingParserDescr

`a...*` is the range of elements greater than or equal to `a`. See also `Std.Rci`.

Equations

- Std.«term_...*» = Lean.ParserDescr.trailingNode `Std.«term_...*» 1024 0 (Lean.ParserDescr.symbol "...*")

Instances For

source
def Std.«term*...*» :
Lean.ParserDescr

`*...*` is the range that is unbounded in both directions. See also `Std.Rii`.

Equations

- Std.«term*...*» = Lean.ParserDescr.node `Std.«term*...*» 1024 (Lean.ParserDescr.symbol "*...*")

Instances For

source
def Std.«term_<...*» :
Lean.TrailingParserDescr

`a<...*` is the range of elements greater than `a`. See also `Std.Roi`.

Equations

- Std.«term_<...*» = Lean.ParserDescr.trailingNode `Std.«term_<...*» 1024 0 (Lean.ParserDescr.symbol "<...*")

Instances For

source
def Std.«term_...<_» :
Lean.TrailingParserDescr

`a...<b` is the range of elements greater than or equal to `a` and less than `b`. See also `Std.Rco`.

Equations

- Std.«term_...<_» = Lean.ParserDescr.trailingNode `Std.«term_...<_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "...<") (Lean.ParserDescr.cat `term 0))

Instances For

source
def Std.«term_..._» :
Lean.TrailingParserDescr

`a...b` is the range of elements greater than or equal to `a` and less than `b`. See also `Std.Rco`.

Equations

- Std.«term_..._» = Lean.ParserDescr.trailingNode `Std.«term_..._» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "...") (Lean.ParserDescr.cat `term 0))

Instances For

source
def Std.«term*...<_» :
Lean.ParserDescr

`*...<b` is the range of elements less than `b`. See also `Std.Rio`.

Equations

- Std.«term*...<_» = Lean.ParserDescr.node `Std.«term*...<_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*...<") (Lean.ParserDescr.cat `term 0))

Instances For

source
def Std.«term*..._» :
Lean.ParserDescr

`*...b` is the range of elements less than `b`. See also `Std.Rio`.

Equations

- Std.«term*..._» = Lean.ParserDescr.node `Std.«term*..._» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*...") (Lean.ParserDescr.cat `term 0))

Instances For

source
def Std.«term_<...<_» :
Lean.TrailingParserDescr

`a<...<b` is the range of elements greater than `a` and less than `b`. See also `Std.Roo`.

Equations

- Std.«term_<...<_» = Lean.ParserDescr.trailingNode `Std.«term_<...<_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "<...<") (Lean.ParserDescr.cat `term 0))

Instances For

source
def Std.«term_<..._» :
Lean.TrailingParserDescr

`a<...b` is the range of elements greater than `a` and less than `b`. See also `Std.Roo`.

Equations

- Std.«term_<..._» = Lean.ParserDescr.trailingNode `Std.«term_<..._» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "<...") (Lean.ParserDescr.cat `term 0))

Instances For

source
def Std.«term_...=_» :
Lean.TrailingParserDescr

`a...=b` is the range of elements greater than or equal to `a` and less than or equal to `b`. See also `Std.Rcc`.

Equations

- Std.«term_...=_» = Lean.ParserDescr.trailingNode `Std.«term_...=_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "...=") (Lean.ParserDescr.cat `term 0))

Instances For

source
def Std.«term*...=_» :
Lean.ParserDescr

`*...=b` is the range of elements less than or equal to `b`. See also `Std.Ric`.

Equations

- Std.«term*...=_» = Lean.ParserDescr.node `Std.«term*...=_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "*...=") (Lean.ParserDescr.cat `term 0))

Instances For

source
def Std.«term_<...=_» :
Lean.TrailingParserDescr

`a<...=b` is the range of elements greater than `a` and less than or equal to `b`. See also `Std.Roc`.

Equations

- Std.«term_<...=_» = Lean.ParserDescr.trailingNode `Std.«term_<...=_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "<...=") (Lean.ParserDescr.cat `term 0))

Instances For

source
class Std.Rxc.IsAlwaysFinite (α : Type u) [PRange.UpwardEnumerable α] [LE α] :
Prop

This type class ensures that right-closed ranges (i.e., for bounds `a` and `b`, `a...=b`, `a<...=b` and `*...=b`) are always finite. This is a prerequisite for many functions and instances, such as `Rcc.toList` or `ForIn'`.

- finite (init hi : α) : ∃ (n : Nat), (PRange.succMany? n init).elim True fun (x : α) => ¬x ≤ hi

Instances

source
class Std.Rxo.IsAlwaysFinite (α : Type u) [PRange.UpwardEnumerable α] [LT α] :
Prop

This type class ensures that right-open ranges (i.e., for bounds `a` and `b`, `a...b`, `a<...b` and `*...b`) are always finite. This is a prerequisite for many functions and instances, such as `Rco.toList` or `ForIn'`.

- finite (init hi : α) : ∃ (n : Nat), (PRange.succMany? n init).elim True fun (x : α) => ¬x < hi

Instances

source
class Std.Rxi.IsAlwaysFinite (α : Type u) [PRange.UpwardEnumerable α] :
Prop

This type class ensures that right-unbounded ranges (i.e., for a bound `a`, `a...*`, `a<...*` and `*...*`) are always finite. This is a prerequisite for many functions and instances, such as `Rci.toList` or `ForIn'`.

- finite (init : α) : ∃ (n : Nat), PRange.succMany? n init = none

Instances

source
instance Std.Rcc.instMembershipOfLE {α : Type u} [LE α] :
Membership α (Rcc α)
Equations

- Std.Rcc.instMembershipOfLE = { mem := fun (r : Std.Rcc α) (a : α) => r.lower ≤ a ∧ a ≤ r.upper }

source
instance Std.Rcc.instDecidableMemOfDecidableLE {α : Type u} {r : Rcc α} {a : α} [LE α] [DecidableLE α] :
Decidable (a ∈ r)
Equations

- Std.Rcc.instDecidableMemOfDecidableLE = inferInstanceAs (Decidable (r.lower ≤ a ∧ a ≤ r.upper))

source
instance Std.Rco.instMembershipOfLEOfLT {α : Type u} [LE α] [LT α] :
Membership α (Rco α)
Equations

- Std.Rco.instMembershipOfLEOfLT = { mem := fun (r : Std.Rco α) (a : α) => r.lower ≤ a ∧ a < r.upper }

source
instance Std.Rco.instDecidableMemOfDecidableLEOfDecidableLT {α : Type u} {r : Rco α} {a : α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] :
Decidable (a ∈ r)
Equations

- Std.Rco.instDecidableMemOfDecidableLEOfDecidableLT = inferInstanceAs (Decidable (r.lower ≤ a ∧ a < r.upper))

source
instance Std.Rci.instMembershipOfLE {α : Type u} [LE α] :
Membership α (Rci α)
Equations

- Std.Rci.instMembershipOfLE = { mem := fun (r : Std.Rci α) (a : α) => r.lower ≤ a }

source
instance Std.Rci.instDecidableMemOfDecidableLE {α : Type u} {r : Rci α} {a : α} [LE α] [DecidableLE α] :
Decidable (a ∈ r)
Equations

- Std.Rci.instDecidableMemOfDecidableLE = inferInstanceAs (Decidable (r.lower ≤ a))

source
instance Std.Roc.instMembershipOfLEOfLT {α : Type u} [LE α] [LT α] :
Membership α (Roc α)
Equations

- Std.Roc.instMembershipOfLEOfLT = { mem := fun (r : Std.Roc α) (a : α) => r.lower < a ∧ a ≤ r.upper }

source
instance Std.Roc.instDecidableMemOfDecidableLEOfDecidableLT {α : Type u} {r : Roc α} {a : α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] :
Decidable (a ∈ r)
Equations

- Std.Roc.instDecidableMemOfDecidableLEOfDecidableLT = inferInstanceAs (Decidable (r.lower < a ∧ a ≤ r.upper))

source
instance Std.Roo.instMembershipOfLT {α : Type u} [LT α] :
Membership α (Roo α)
Equations

- Std.Roo.instMembershipOfLT = { mem := fun (r : Std.Roo α) (a : α) => r.lower < a ∧ a < r.upper }

source
instance Std.Roo.instDecidableMemOfDecidableLT {α : Type u} {r : Roo α} {a : α} [LT α] [DecidableLT α] :
Decidable (a ∈ r)
Equations

- Std.Roo.instDecidableMemOfDecidableLT = inferInstanceAs (Decidable (r.lower < a ∧ a < r.upper))

source
instance Std.Roi.instMembershipOfLT {α : Type u} [LT α] :
Membership α (Roi α)
Equations

- Std.Roi.instMembershipOfLT = { mem := fun (r : Std.Roi α) (a : α) => r.lower < a }

source
instance Std.Roi.instDecidableMemOfDecidableLT {α : Type u} {r : Roi α} {a : α} [LT α] [DecidableLT α] :
Decidable (a ∈ r)
Equations

- Std.Roi.instDecidableMemOfDecidableLT = inferInstanceAs (Decidable (r.lower < a))

source
instance Std.Ric.instMembershipOfLE {α : Type u} [LE α] :
Membership α (Ric α)
Equations

- Std.Ric.instMembershipOfLE = { mem := fun (r : Std.Ric α) (a : α) => a ≤ r.upper }

source
instance Std.Ric.instDecidableMemOfDecidableLE {α : Type u} {r : Ric α} {a : α} [LE α] [DecidableLE α] :
Decidable (a ∈ r)
Equations

- Std.Ric.instDecidableMemOfDecidableLE = inferInstanceAs (Decidable (a ≤ r.upper))

source
instance Std.Rio.instMembershipOfLT {α : Type u} [LT α] :
Membership α (Rio α)
Equations

- Std.Rio.instMembershipOfLT = { mem := fun (r : Std.Rio α) (a : α) => a < r.upper }

source
instance Std.Rio.instDecidableMemOfDecidableLT {α : Type u} {r : Rio α} {a : α} [LT α] [DecidableLT α] :
Decidable (a ∈ r)
Equations

- Std.Rio.instDecidableMemOfDecidableLT = inferInstanceAs (Decidable (a < r.upper))

source
instance Std.Rii.instMembership {α : Type u} :
Membership α (Rii α)
Equations

- Std.Rii.instMembership = { mem := fun (x : Std.Rii α) (x_1 : α) => True }

source
instance Std.Rii.instDecidableMem {α : Type u} {r : Rii α} {a : α} :
Decidable (a ∈ r)
Equations

- Std.Rii.instDecidableMem = inferInstanceAs (Decidable True)

source
class Std.Rcc.HasRcoIntersection (α : Type w) :
Type w

This type class allows taking the intersection of a closed range with a left-closed right-open range, resulting in another left-closed right-open range.

- intersection : Rcc α → Rco α → Rco α

Instances

source
class Std.Rcc.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] :
Prop

This type class ensures that the intersection according to `Rcc.HasRcoIntersection` of two ranges contains exactly those elements that are contained in both ranges.

- mem_intersection_iff {a : α} {r : Rcc α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

Instances

source
class Std.Rco.HasRcoIntersection (α : Type w) :
Type w

This type class allows taking the intersection of two left-closed right-open ranges, resulting in another left-closed right-open range.

- intersection : Rco α → Rco α → Rco α

Instances

source
class Std.Rco.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] :
Prop

This type class ensures that the intersection according to `Rco.HasRcoIntersection` of two ranges contains exactly those elements that are contained in both ranges.

- mem_intersection_iff {a : α} {r s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

Instances

source
class Std.Rci.HasRcoIntersection (α : Type w) :
Type w

This type class allows taking the intersection of a left-closed right-unbounded range with a left-closed right-open range, resulting in another left-closed right-open range.

- intersection : Rci α → Rco α → Rco α

Instances

source
class Std.Rci.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] :
Prop

This type class ensures that the intersection according to `Rci.HasRcoIntersection` of two ranges contains exactly those elements that are contained in both ranges.

- mem_intersection_iff {a : α} {r : Rci α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

Instances

source
class Std.Roc.HasRcoIntersection (α : Type w) :
Type w

This type class allows taking the intersection of a left-open right-closed range with a left-closed right-open range, resulting in another left-closed right-open range.

- intersection : Roc α → Rco α → Rco α

Instances

source
class Std.Roc.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] :
Prop

This type class ensures that the intersection according to `Roc.HasRcoIntersection` of two ranges contains exactly those elements that are contained in both ranges.

- mem_intersection_iff {a : α} {r : Roc α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

Instances

source
class Std.Roo.HasRcoIntersection (α : Type w) :
Type w

This type class allows taking the intersection of an open range with a left-closed right-open range, resulting in another left-closed right-open range.

- intersection : Roo α → Rco α → Rco α

Instances

source
class Std.Roo.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] :
Prop

This type class ensures that the intersection according to `Roo.HasRcoIntersection` of two ranges contains exactly those elements that are contained in both ranges.

- mem_intersection_iff {a : α} {r : Roo α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

Instances

source
class Std.Roi.HasRcoIntersection (α : Type w) :
Type w

This type class allows taking the intersection of a left-open right-unbounded range with a left-closed right-open range, resulting in another left-closed right-open range.

- intersection : Roi α → Rco α → Rco α

Instances

source
class Std.Roi.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] :
Prop

This type class ensures that the intersection according to `Roi.HasRcoIntersection` of two ranges contains exactly those elements that are contained in both ranges.

- mem_intersection_iff {a : α} {r : Roi α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

Instances

source
class Std.Ric.HasRcoIntersection (α : Type w) :
Type w

This type class allows taking the intersection of a left-unbounded right-closed range with a left-closed right-open range, resulting in another left-closed right-open range.

- intersection : Ric α → Rco α → Rco α

Instances

source
class Std.Ric.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] :
Prop

This type class ensures that the intersection according to `Ric.HasRcoIntersection` of two ranges contains exactly those elements that are contained in both ranges.

- mem_intersection_iff {a : α} {r : Ric α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

Instances

source
class Std.Rio.HasRcoIntersection (α : Type w) :
Type w

This type class allows taking the intersection of a left-unbounded right-open range with a left-closed right-open range, resulting in another left-closed right-open range.

- intersection : Rio α → Rco α → Rco α

Instances

source
class Std.Rio.LawfulRcoIntersection (α : Type w) [LT α] [LE α] [HasRcoIntersection α] :
Prop

This type class ensures that the intersection according to `Rio.HasRcoIntersection` of two ranges contains exactly those elements that are contained in both ranges.

- mem_intersection_iff {a : α} {r : Rio α} {s : Rco α} : a ∈ HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s

Instances