Argv.followup: def of bolt@1.27.0.0
Import: import bolt@1.27.0.0/src/lsp/checker/argv.bend as Argv
Lines 36-41 of bolt@1.27.0.0/src/lsp/checker/argv.bend: https://jend.leeeet.dev/read.txt?path=bolt@1.27.0.0/src/lsp/checker/argv.bend&start_line=36&end_line=41

import Base
import bolt@1.27.0.0/src/paths.bend as Paths
import bolt@1.27.0.0/src/lsp/report.bend as Rep

# By convention LAWS.bend states its laws as open claims and PROOF.bend, beside
# it, fills them: alone, LAWS.bend always has TODOs. They are an error only
# while PROOF.bend does not check clean, so a first report that is only the
# open laws of a LAWS.bend is followed by a run on that PROOF.bend
def followup(+ds: List<&2, Rep.Diag>, +path: String) -> Maybe<&2, Run>:
  Bool.pick(Maybe<&2, Run>, Bool.and(only_todos(ds), Paths.is_laws(path)), Some{run_of(proof_path(path))}, None{})

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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=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/lsp/checker/argv.bend&name=Run
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/lsp/checker/argv.bend&name=only_todos
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/lsp/checker/argv.bend&name=proof_path
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/lsp/checker/argv.bend&name=run_of
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/lsp/report.bend&name=Diag
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/paths.bend&name=is_laws