[v0.5] SP-17 writes down what it cannot see and matches its allow-list exactly (follow-up to #167) #181

Follow-up to #167 (review of #163). SP-17's scan (crates/conformance/src/lean_literals.rs:291, scope :400-422):

• reads one string literal at a time, so a template split with concat! or + passes;
• decodes no escape but \n;
• reads only .rs files, and only part of backend/lean.rs, from line 2398.

A Python port of its test accepted "private theorem {n} : {t}\n by decide", "inductive {t} where\n | a", "end {ns}", "#reduce {}" and "by simp [{}]". Its allow-list matches by prefix, so the " := " entry (:87) admits any literal that starts with :=.

Definition of done:

• The scan joins adjacent literals as RT-04 does, decodes escapes, and covers the whole of backend/lean.rs, or VERIFICATION.md names each unread shape, as RT-04's section does.
• The allow-list matches whole literals.
• Each listed shape is planted and found, and the plants are recorded.
• just vv green.

Generated by Claude Code