Skip to content

Fix Refinement Declaration Positions - #331

Open
rcosta358 wants to merge 1 commit into
codex/smt-unknown-errorfrom
codex/refinement-declaration-position
Open

rcosta358 wants to merge 1 commit into
codex/smt-unknown-errorfrom
codex/refinement-declaration-position

Conversation

@rcosta358

@rcosta358 rcosta358 commented Oct 5, 2026 •

Copy link
Copy Markdown
Collaborator

Description

Highlight the predicate in “Refinement declared here” diagnostics by reading its annotation position directly, removing the dependency on parsing order.

Example

Before

image

After

image

Validation: 206 tests passed, including declaration-position regression tests.

Related Issues

Stacked on #330. Merge it first, then retarget to main.

🤖 Generated with Codex

Co-authored-by: Codex <noreply@openai.com>
@rcosta358 rcosta358 added bug Something isn't working error messages Related to error messages labels Oct 5, 2026
@rcosta358 rcosta358 changed the title Highlight predicates in refinement declaration diagnostics Fix Refinement Declaration Positions Oct 5, 2026
@rcosta358
rcosta358 added this pull request to stack #332 October 5, 2026 14:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Something isn't working error messages Related to error messages

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant