def proofs

bolt@1.27.0.0 · src/rules/digest.bend:210

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

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