Skip to content

Preserve symbolic List frames in matcher residuals (adopted) - #4163

Merged
jberthold merged 3 commits into
masterfrom
fix/list-frame-matcher-4161-adopted
Sep 30, 2026
Merged

jberthold merged 3 commits into
masterfrom
fix/list-frame-matcher-4161-adopted

Conversation

@jberthold

Copy link
Copy Markdown
Collaborator

Branch adopted from PR #4162

Fixes #4161.

Build the unmatched List residual as remainingPrefix ++ subjectFrame instead of inserting the List frame as an element. Add regressions for empty and nonempty remaining prefixes.

Validation: both regressions fail before the fix; all 5,188 Kore tests pass. Fourmolu and HLint pass.

@jberthold
jberthold requested a review from ehildenb September 29, 2026 14:22
@jberthold

jberthold commented Sep 29, 2026 •

Copy link
Copy Markdown
Collaborator Author

Test added in #3751 falls in CI now on simplifying size(?L) + 2 > 0 , apparently there is no simplification to state that size(_:List) >=Int 0 or similar.

@jberthold
jberthold merged commit d84a541 into master Sep 30, 2026
11 of 12 checks passed
@jberthold
jberthold deleted the fix/list-frame-matcher-4161-adopted branch September 30, 2026 12:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

List matcher treats a symbolic List frame as an element, allowing false proofs

3 participants