Bind.push_name: def of bolt@1.27.0.0
Import: import bolt@1.27.0.0/src/syntax/bind.bend as Bind
Lines 130-138 of bolt@1.27.0.0/src/syntax/bind.bend: https://jend.leeeet.dev/read.txt?path=bolt@1.27.0.0/src/syntax/bind.bend&start_line=130&end_line=138

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

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/lazy/lazy.bend&name=stop
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/syntax/bind.bend&name=push_name.again