Imports.fresh.spec: def of bolt@1.27.0.0
Import: import bolt@1.27.0.0/src/rules/imports.bend as Imports
Lines 86-95 of bolt@1.27.0.0/src/rules/imports.bend: https://jend.leeeet.dev/read.txt?path=bolt@1.27.0.0/src/rules/imports.bend&start_line=86&end_line=95

import Base

# the files of ds that were read and are not yet seen, each once: the spec
# fresh.fast is proven against (imp.fresh)
def fresh.spec(ds: List<&2, String>, +seen: List<&2, String>, +read: List<&2, String>) -> List<&2, String>:
  match ds:
    case Nil{}:
      Nil{}
    case Con{+d, rest}:
      +more = fresh.spec(rest, seen, read)
      +known = Bool.and(has(read, d), Bool.not(has(seen, d)))
      Bool.pick(List<&2, String>, Bool.and(known, Bool.not(has(more, d))), d <> more, more)

Uses (6):
  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.not
  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/imports.bend&name=has