class AA create make feature make local b: BB do create b f (b) end feature {ANY} f (b1: BB) require (agent (b: BB): BOOLEAN local c: BB do -- Unfolded form of 'across b as c all True end'. from c := b.new_cursor c := b -- Make sure that `c` is considered as attached to avoid other errors below. Result := True until c.after or not Result loop Result := True c.forth end end).item ([b1]) do print ("Failed") end end