src/rules/correctness/hole.bend fails

raw source on the hub · import 0xde9bb08f7de298b03207fb5797ede9a5/src/rules/correctness/hole.bend as Hole

rule hole: a TODO hole left in code, the one bend counts in "N TODO found": a ? and then the name TODO, with any spaces, newlines or comments between them (?TODO, ? TODO). ?todo, ?TODO_later and ?TODO.x are other names, which bend reports as a type error, not as a TODO, and they are not reported here. The finding spans ? through TODO when both sit on one line, and the ? alone when TODO is on a later line. LAWS.bend is exempt: by convention its laws are open claims, filled by PROOF.bend beside it.

7 imports

import Base
import ../../paths.bend as Paths
import ../../src.bend as Src
import ../../finding.bend as F
import ../../syntax/lex.bend as Lex
import ../../lazy/lazy.bend as Lazy
import ../calls.bend as Calls

The reader could not load this file (at 0xde9bb08f7de298b03207fb5797ede9a5/src/config.bend:32). What bend.ts says:

Error:
- expected : a fresh name (duplicate declaration: Set)
- observed : 'Set'
Location:
31 | # a name (a group's or a rule's) at a level
32>| type Set is Data:
   |      ^^^
33 |   Set{name: String, level: Level}