@[inline]

def Std.Iter.empty (β : Type w) : Iter β

Returns an iterator that terminates immediately.

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• Std.Iter.empty β = (Std.IterM.empty Id β).toIter