Skip to content

docs: make consumer guidance integration-neutral #5

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
kim-em merged 1 commit into from
Aug 25, 2026
Merged

docs: make consumer guidance integration-neutral #5

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
10 changes: 4 additions & 6 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,7 @@ The benchmark context is still required in schema version 1 to resolve trusted i
modules and declaration spans from `.ilean` data. A future wire version can
replace that context with an explicit dependency bundle without changing schema version 1.

The consumer owns hole resolution. This matches the interface needed by the
Formal Conjectures importer: it can resolve declarations under LeanEval's
pinned target environment, then pass the resulting ranges and dependency data
to this renderer. Formal Conjectures fixtures are intentionally not copied or
modified in this foundation package; they should be added by their importer
owners when that consumer switches to the contract.
The consumer owns hole resolution. A consumer resolves declarations under its
pinned target environment, then passes the resulting ranges and dependency
data to this renderer. Consumer-specific fixtures and source trees do not
belong in this foundation package.