bolt/rules/laws/closed.bend fails

raw source on the hub · import 0x729eecea86ea5a2cdba3a2856a313bca/bolt/rules/laws/closed.bend as Closed

rule closed: a law in a LAWS.bend with no for or exs binder. It states one closed fact (law sanity: {U32.add(2, 3) == 5 : U32}), which the checker proves by computing it: a test, not a claim about every input, and a law cut down that way hides that the general one no longer holds. State it over a for x: T (or ask for an exs witness). Laws outside LAWS.bend are not held to it.

6 imports

import Base
import ../../src.bend as Src
import ../../finding.bend as F
import ../../../syntax/tree.bend as Tree
import ../../../lazy/lazy.bend as Lazy
import ../../../syntax/bind.bend as Bind

The reader could not load this file (at 0x729eecea86ea5a2cdba3a2856a313bca/bolt/config.bend:31). What bend.ts says:

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