DEVIATIONS.md draws the line: a technical consequence in Lean is content, an
editorial preference is meta and belongs in DEVIATIONS.md. Two passages are
on the wrong side of it.
CSwL/Games/SeaBattle.lean:78 — "as colunas poderiam ter sido modeladas
como as linhas, o que tornaria o design mais simples. Mas preferimos seguir
o estilo de coordenadas usual". The clearest case: it reports what the
authors decided.CSwL/Games/SeaBattle.lean:144 — "Preferimos manter Game como está e
formalizar a propriedade…". Harder, because it explains why the code does
not match the grammar the previous exercise asks the reader to revise, and
deleting it leaves the reader wondering. The fix is probably to state the
predicate on its own terms rather than to cut the paragraph.
CSwL/English.lean:311 ("Nossa gramática poderia ser:") was checked and is a
false positive — it introduces a grammar, it does not defend a choice.
Recorded so a later sweep does not re-litigate it.
DEVIATIONS.mddraws the line: a technical consequence in Lean is content, aneditorial preference is meta and belongs in
DEVIATIONS.md. Two passages areon the wrong side of it.
CSwL/Games/SeaBattle.lean:78— "as colunas poderiam ter sido modeladascomo as linhas, o que tornaria o design mais simples. Mas preferimos seguir
o estilo de coordenadas usual". The clearest case: it reports what the
authors decided.
CSwL/Games/SeaBattle.lean:144— "Preferimos manterGamecomo está eformalizar a propriedade…". Harder, because it explains why the code does
not match the grammar the previous exercise asks the reader to revise, and
deleting it leaves the reader wondering. The fix is probably to state the
predicate on its own terms rather than to cut the paragraph.
CSwL/English.lean:311("Nossa gramática poderia ser:") was checked and is afalse positive — it introduces a grammar, it does not defend a choice.
Recorded so a later sweep does not re-litigate it.