Digest.proofs: def of bolt@1.27.0.0
Import: import bolt@1.27.0.0/src/rules/digest.bend as Digest
Lines 210-220 of bolt@1.27.0.0/src/rules/digest.bend: https://jend.leeeet.dev/read.txt?path=bolt@1.27.0.0/src/rules/digest.bend&start_line=210&end_line=220

import Base
import bolt@1.27.0.0/src/rules/calls.bend as Calls

# the names of the top-level defs that are proofs (Calls.proof: one that
# returns a proof, or one written with no type, which is how Bend fills the
# law named f). The law states their property, so the coverage rule neither
# grades them nor walks through them
def proofs(ds: List<&2, Calls.Def>) -> List<&2, String>:
  match ds:
    case Nil{}:
      Nil{}
    case Con{Calls.Def{name, +sig, body}, rest}:
      +more = proofs(rest)
      Bool.pick(List<&2, String>, Calls.proof(sig), name <> more, more)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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/rules/calls.bend&name=Def
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/rules/calls.bend&name=proof