feat(tg-11): surface syntax for epistemic types + fix a second statement-order bug - #99
Conversation
…ent-order bug TG-11 landed the type former, typing, evaluation and six proofs — but there was no way to WRITE one. Zero occurrences of the constructors in lexer.mll or parser.mly, against 4 for echo. Fully implemented and unreachable. ## Surface syntax warrant[k](claim, evidence) -- at standpoint k evidence(w) -- the ONLY elimination The standpoint is bracketed because it is an index, not an operand — the same reading as a braid generator's subscript. Non-factivity reaches the syntax too: there is deliberately NO keyword that extracts the claim. `claim(w)` parses as an ordinary call to an undefined function, never as a language form, and a test pins that distinction — if a `Claim` form ever appears, it contradicts epi_only_yields_evidence. No grammar conflicts. ## A SECOND copy of the statement-order bug Writing the first epistemic program surfaced it. `def w = warrant[...]` then `def tok = evidence(w)` failed with In definition 'tok': evidence requires an Epi[k, rho, tau], got Word[0] The Word[0] is the pass-1a placeholder: `tok` was being checked BEFORE `w` had been refined. Same root cause as #95 — `stmts := prog @ !stmts` followed by `List.rev` on the flattened list — but in a SECOND copy, in lib/check.ml. That copy feeds `tanglec --check` AND the LSP, so both have been analysing programs with their statements reversed. It was not epistemic-specific: def e = echoClose(braid[s1]) def r = residue(e) -- "residue requires Echo[_, _], got Word[0]" Any cross-definition reference to a non-Word type was mis-typed. Echo has been broken this way for as long as the recovering path has existed. Fixed identically: accumulate segments, flatten in order. The test suites missed BOTH copies because they call Parser.program directly and never exercise the recovering path. ## Tests Parser: warrant with bracketed standpoint, evidence, TG-4 round-trip, and the no-claim-form guard. Check: three cross-definition cases — plain, echo, and epistemic — that would all have failed before. examples/epistemic.tangle added and wired into the corpus gate's must-run set: warrants at three standpoints, evidence recovery, and the echo composition (`residue(evidence(we))`). All assertions pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Uh oh!
There was an error while loading. Please reload this page.
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review✅ ApprovedAdds surface syntax for epistemic types and fixes a statement-order bug in the checker that caused cross-definition references to resolve placeholders. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
TG-11 (#98) landed the type former, typing, evaluation and six proofs — but there was no way to write one. Zero occurrences of the constructors in
lexer.mllorparser.mly, against 4 for echo. Fully implemented and unreachable.Surface syntax
The standpoint is bracketed because it's an index, not an operand — the same reading as a braid generator's subscript. No grammar conflicts.
Non-factivity reaches the syntax. There is deliberately no keyword extracting the claim:
claim(w)parses as an ordinary call to an undefined function, never as a language form. A test pins that distinction — if aClaimform ever appears, it contradictsepi_only_yields_evidence.A second copy of the statement-order bug
Writing the first epistemic program surfaced it immediately:
That
Word[0]is the pass-1a placeholder —tokwas being checked beforewwas refined. Same root cause as #95 (stmts := prog @ !stmtsthenList.revon the flattened list), but in a second copy, inlib/check.ml.That copy feeds
tanglec --checkand the LSP. Both have been analysing programs with their statements reversed.And it was never epistemic-specific:
Any cross-definition reference to a non-
Wordtype was mis-typed. Echo has been broken this way for as long as the recovering path has existed.The test suites missed both copies for the same reason: they call
Parser.programdirectly and never exercise the recovering path.Tests
Parser — warrant with bracketed standpoint; evidence; TG-4 round-trip; the no-claim-form guard.
Check — three cross-definition cases (plain, echo, epistemic), all of which would have failed before this.
Example
examples/epistemic.tangle, wired into the corpus gate's must-run set — warrants at three standpoints, evidence recovery, and the echo compositionresidue(evidence(we)). All assertions pass.It also documents why the claim is unreachable: if it were extractable, anything anyone attested would become true by fiat — precisely the bug you don't want in a provenance system.
All gates green: Lean 0 errors, full suite, corpus, RSR.
🤖 Generated with Claude Code