Follow-up from #72.
Since #72, Line carries inference : Option Source and ArgumentPackage carries inferences : List Source. These are load-bearing: Dispute.rankOf gives every step the rank of its package's weakest cited inference, and Dispute.rated requires each node to have one. The verdict of isaiahDispute changes when one of them is re-rated (see the issue on answering Postell's parity inference).
Neither generator shows them. Testimony/Tools/Pages.lean, Logic/Markdown.lean and Logic/Latex.lean never read inference or inferences. So a reader of docs/src/arguments/*.md or arguments.pdf sees:
- each premise with its citation and confidence;
- the step as a formula;
- nothing on who is cited for the step or how it is rated, except where a line docstring happens to say so in prose.
The rating reasons are currently Lean comments inside the Line (for example the disputed note on ordinarySignLine), and comments are not harvested.
To do
- Harvest each
Line's inference and render it next to the step: the citation (linked to the bibliography like any other cite key) and its confidence.
- Decide whether the reason for a rating belongs in the
Source itself (a note field) or stays in the docstring. The first keeps it next to the rating it justifies, the second needs no new field. Either way it should reach the page.
- Update
reading-the-logic.md, which describes what a line on the page shows.
- Regenerate with
lake exe argdoc and lake exe argtex. Every --check must pass.
Follow-up from #72.
Since #72,
Linecarriesinference : Option SourceandArgumentPackagecarriesinferences : List Source. These are load-bearing:Dispute.rankOfgives every step the rank of its package's weakest cited inference, andDispute.ratedrequires each node to have one. The verdict ofisaiahDisputechanges when one of them is re-rated (see the issue on answering Postell's parity inference).Neither generator shows them.
Testimony/Tools/Pages.lean,Logic/Markdown.leanandLogic/Latex.leannever readinferenceorinferences. So a reader ofdocs/src/arguments/*.mdorarguments.pdfsees:The rating reasons are currently Lean comments inside the
Line(for example thedisputednote onordinarySignLine), and comments are not harvested.To do
Line'sinferenceand render it next to the step: the citation (linked to the bibliography like any other cite key) and its confidence.Sourceitself (anotefield) or stays in the docstring. The first keeps it next to the rating it justifies, the second needs no new field. Either way it should reach the page.reading-the-logic.md, which describes what a line on the page shows.lake exe argdocandlake exe argtex. Every--checkmust pass.