def seen.holds

ezx@1.11.0.0 · src/lock/lock.bend:411

import Base

411# whether a name is already among the ones a walk has seen. Base's
412# `List.contains` applies an erased equality, which Bend's termination check
413# cannot see through; this scan is structural. `any.step` is what lets it
414# stop at the name it was looking for instead of reading past it.
415def seen.holds(xs: List<&2, String>, +needle: String) -> Bool:
416  match xs:
417    case []:
418      False{}
419    case +h <> t:
420      any.step(String.eq(h, needle), _u => seen.holds(t, needle))