Range iterator

This module provides iterators over ranges Std.Rcc (and Std.Rco, ...) via Std.Rcc.iter (and Std.Rco.iter, ...).

@[inline]

def Std.Rcc.iter {α : Type u_1} (r : Rcc α) : Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• r.iter = { internalState := { next := some r.lower, upperBound := r.upper } }

@[inline]

def Std.Rco.iter {α : Type u_1} (r : Rco α) : Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• r.iter = { internalState := { next := some r.lower, upperBound := r.upper } }

@[inline]

def Std.Rci.iter {α : Type u_1} (r : Rci α) : Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• r.iter = { internalState := { next := some r.lower } }

@[inline]

def Std.Roc.iter {α : Type u_1} [PRange.UpwardEnumerable α] (r : Roc α) : Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• r.iter = { internalState := { next := Std.PRange.succ? r.lower, upperBound := r.upper } }

@[inline]

def Std.Roo.iter {α : Type u_1} [PRange.UpwardEnumerable α] (r : Roo α) : Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• r.iter = { internalState := { next := Std.PRange.succ? r.lower, upperBound := r.upper } }

@[inline]

def Std.Roi.iter {α : Type u_1} [PRange.UpwardEnumerable α] (r : Roi α) : Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• r.iter = { internalState := { next := Std.PRange.succ? r.lower } }

@[inline]

def Std.Ric.iter {α : Type u_1} [PRange.Least? α] (r : Ric α) : Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• r.iter = { internalState := { next := Std.PRange.least?, upperBound := r.upper } }

@[inline]

def Std.Rio.iter {α : Type u_1} [PRange.Least? α] (r : Rio α) : Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• r.iter = { internalState := { next := Std.PRange.least?, upperBound := r.upper } }

@[inline]

def Std.Rii.iter {α : Type u_1} [PRange.Least? α] : Rii α → Iter α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

Equations

• x✝.iter = { internalState := { next := Std.PRange.least? } }