docs: style guides, contributor guide, and a student README

[arademaker]

Project documentation adapted from sf-in-lean, plus the retirement of
TODO.md in favour of GitHub issues.

What this adds

Three new documents, and the wiring so the existing ones point at them rather
than duplicating them.

STYLE-CODE.md — Lean and Verso conventions. Its core is a ledger of
which Lean feature is first used in which chapter, derived from a sweep of the
code inside ```lean blocks. It makes checkable the constraint
DEVIATIONS.md already states — nothing is used before it is presented —
which until now was verified by hand. Because this book is mostly programs
rather than proofs, the ledger covers every Lean feature, not only tactics.

It also documents the directive vocabulary that CSwLMeta/ already
implements (:::exercise, solution!, :::gradeTheorem, :::dev,
:::quiz, the four build variants) and that had no documentation anywhere:
writing a chapter previously meant reading the elaborator.

STYLE-WRITING.md — prose conventions. Absorbs the "Pedagogical
decisions" section out of CLAUDE.md, adds writing advice adapted from
sf-in-lean, and starts a Portuguese term list. That list is deliberately
short: it records decisions actually taken, because prescribing a term the
book has never used against an alternative it has never used is the same
failure the section exists to catch.

CONTRIBUTING.md — workflow, and who decides what. Written for the
situation this repository is actually in: one author, with the course monitor
as alpha tester. Content and structure stay with the author; the objective
tasks open to a contributor are listed explicitly. The coordination machinery
sf-in-lean needs for several contributors across branches — Zulip, CODEOWNERS,
the branch-activity dashboard, the draft-PR protocol — is deliberately absent.

Its AI policy is this project's own rather than sf-in-lean's, which forbids
AI-written prose outright and would contradict CLAUDE.md: here AI never
writes prose on its own initiative, translates as literally as the target
language allows, and produces drafts for human revision.

Findings from the sweep

Writing the ledger meant reading the chapters against the rule, which turned
up things now filed as issues:

• :::dev notes reach the student, in the HTML and in the generated Lean,
  in every variant — including the terse project opened in class (:::dev notes reach the student, in the HTML and in the generated Lean #4).
• native_decide, trivial, injection and one Fintype instance are used
  without being presented (Lean features used without being presented #7).
• Two paragraphs defend an editorial choice in the book's prose, which
  DEVIATIONS.md says belongs in DEVIATIONS.md (Two paragraphs defend an editorial choice in the book's prose #5).

Two things I initially reported as violations turned out not to be, and the
ledger records why: IntroCS's use of unpresented Lean is the constraint's
one accepted exception, and simp/decide are presented — in a plain-text
table that a scan of lean blocks does not see. STYLE-CODE.md now carries
that caveat so the next sweep does not repeat the mistake.

One behaviour change

CSwLMeta/Save/Project.lean — the generated project's README.md was in
Portuguese and said only "não edite aqui". It is now in English, like every
other document about the project, and the student variant carries a real
setup guide: how to build, how to work an exercise, where to report a problem.
That variant is what reaches the students at emap-nlp/book.

TODO.md is gone

Its 20 open items were consolidated into GitHub issues #3–#20; everything it
recorded as done was discarded rather than filed to be closed. Issue #3 is the
umbrella for the restructuring the rest of them depend on.

Note on scope

This branch also carries 0d16e25 drafts, which is unrelated teaching
material. The documentation work is d9db3e5.

Uncommitted and deliberately left out: prose edits in PL.lean and
FOL.lean, and working notes under doc/.

AI usage

The documents were drafted with Claude Code (Opus 5) from decisions taken in
conversation, with the author directing scope, rejecting several proposals,
and reviewing the result. The feature ledger was derived by script from the
chapter sources and corrected by hand where the scan proved too narrow. This
description was likewise AI-drafted and reviewed.

[Copilot]

🟡 Changes recommended

Documentation inaccuracies and scope inconsistencies should be corrected before approval.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

Adds project style guides, contributor workflow documentation, and English setup guidance for generated student projects while moving pending work from TODO.md to GitHub issues.

Changes:

• Adds Lean/Verso and Portuguese writing conventions.
• Updates contributor and project documentation.
• Updates generated READMEs and includes FOL teaching drafts.

File summaries

File	Reviewed changes
STYLE-WRITING.md	Prose and Portuguese writing conventions
STYLE-CODE.md	Lean, Verso, variants, and feature-ledger conventions
README.md	Links to normative documentation
doc/fol-semantics.md	FOL semantics teaching notes
doc/entailment.md	Entailment teaching notes
DEVIATIONS.md	Project deviations and issue tracking
CSwLMeta/Save/Project.lean	Generates English student project READMEs
CSwL/Logic/FOL.lean	Adjusts code warning line length
CONTRIBUTING.md	Contributor workflow and AI policy
CLAUDE.md	References the style guides

Review details

Suppressed comments (6)

README.md:72

• This repeats the inaccurate description that CSwL/Games.lean only gathers included sections; the file also contains chapter-level introductory prose before the includes. Please describe it as gathering sections while allowing introductory prose, so this overview agrees with the actual glue file and the normative style guide.

Mnemonic file names, never numbers. A short chapter is a single file
(`CSwL/Sets.lean`, `namespace Sets`); a chapter whose sections are long enough
to deserve their own file is a "glue" file (`CSwL/Games.lean`) that only
gathers them, via `{include 1 ...}`, from a same-named directory

STYLE-CODE.md:85

• These lines say the explanation is hidden inside the solution, but CSwL/Morphology/SwedishPlural.lean:63-66 is a comment outside the solution! markers, so it survives the student source rewrite. The actual problem is that it is a Portuguese Lean comment; please correct this description and decide whether to promote the explanation to prose or rewrite the comment in English.

  appears, and a comment at `:63-66` says why, but that comment is inside the
  solution and in Portuguese, so the explanation reaches neither the student
  nor the English code-comment rule.

STYLE-CODE.md:178

• :::dev is not currently filtered by variant: Block.devcomment.traverse returns none unconditionally, and the extractor emits shown notes without consulting getCurrVariant. Thus the existing no-urgency note in CSwL/Logic/FOL.lean appears in the student and terse HTML/generated Lean, so this guarantee is false until issue #4 is implemented.

- `:::dev` — an internal note to the authors. It renders with the heading
  "Nota editorial" and must never carry anything the student should not read.
  AI-generated commentary belongs here and is marked as such.

STYLE-CODE.md:124

• CSwL/Games.lean is not only an include aggregator: it also contains the chapter's introductory prose at lines 12–21 before the two includes. Calling this a file that “only gathers” sections gives contributors an incorrect model of where chapter-level prose belongs.

A short chapter is a single file (`CSwL/Sets.lean`). A chapter whose sections
are long enough to deserve their own files is a "glue" file (`CSwL/Games.lean`)
that only gathers them via `{include 1 …}` from a same-named directory. Each

doc/entailment.md:111

• A complete theory is one that decides every formula—typically, for each φ, either Γ ⊨ φ or Γ ⊨ ¬φ; it is not generally defined by having a single model or valuation. If uniqueness is only the property of this finite example, state it as the reason completeness follows here rather than as the definition.

* **teoria completa:** \(\Gamma\) restringe as interpretações a uma única valuation, nesse exemplo.

doc/entailment.md:111

• valuation is left in English inside this Portuguese note, while the surrounding logic chapters consistently use valoração. That makes the term look like a second concept; use the established Portuguese term.

* **teoria completa:** \(\Gamma\) restringe as interpretações a uma única valuation, nesse exemplo.

• Files reviewed: 10/10 changed files
• Comments generated: 5
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[arademaker]

done locally

[arademaker]

solved locally