Skip to content

doc(AGENTS): quotations are copied from the pinned source or labeled paraphrase #1072

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 1 commit into from
Oct 25, 2026
Merged

doc(AGENTS): quotations are copied from the pinned source or labeled paraphrase #1072

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions AGENTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -396,8 +396,11 @@ and [API review with explicit nonblocking nits](https://github.com/leanprover/cs

When a declaration claims to formalize a cited result, the PR quotes the source statement with its
exact locator and maps the source's notation to the Lean statement: quantifiers, models, encodings
and resource conventions. Reviewers check that mapping rather than an impression. New mathematics
and new proof ideas need no source; label them as original.
and resource conventions. Reviewers check that mapping rather than an impression. Text presented as
a quotation is copied from the pinned source version, with its locator checked there rather than
taken from an issue, a PR or other library text; anything else is labeled as a paraphrase. Reviewers
check quotations against the source, and a quoted passage that is not in the source blocks approval.
New mathematics and new proof ideas need no source; label them as original.

Whether a new definition needs checked examples on both sides (an instance where it holds and one
where it fails) is for the author and reviewers to judge; reviewers may ask for them when a
Expand Down
Loading