src/rules/correctness/arms.bend fails

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

rule arms: a Nat arm no value can reach. case kn+p: matches every Nat from k up, so a later case jn+q: with j >= k, or a later case mn: with m >= k, never runs. The checker accepts it and the match quietly returns the earlier arm (nohzafk pat_bad: 0n, 1n+p, 2n+p gives f(2n) = 1; bend 2.0.16 still does). Put the narrower arms first: the literals, then the larger n+p. Succ{p} and Succ{_} count as 1n+p. Only a single-scrutinee match is read: a column of a multi-scrutinee match is skipped.

7 imports

import Base
import ../../src.bend as Src
import ../../finding.bend as F
import ../../syntax/lex.bend as Lex
import ../../syntax/tree.bend as Tree
import ../../lazy/lazy.bend as Lazy
import ../tokens.bend as T

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}