def push_name

bolt@1.27.0.0 · src/syntax/bind.bend:130

import Base
import bolt@1.27.0.0/src/lazy/lazy.bend as Lazy

130# a name, when there is one, onto a list, unless it is the name just put
131# there: a proof file's `law x` and its `def x` are one item, and every use
132# no binder holds is looked for in this list
133def push_name(mm: Maybe<&2, String>, +acc: List<&2, String>) -> List<&2, String>:
134  match mm:
135    case None{}:
136      acc
137    case Some{+name}:
138      Lazy.stop(List<&2, String>, push_name.again(acc, name), acc, _u => name <> acc)