Skip to content

Add error checking for nested datatypes#373

Merged
shigoel merged 18 commits intomainfrom
josh/nested-type
Feb 5, 2026
Merged

Add error checking for nested datatypes#373
shigoel merged 18 commits intomainfrom
josh/nested-type

Conversation

@joscoh
Copy link
Copy Markdown
Contributor

@joscoh joscoh commented Feb 2, 2026

Issue #, if available: #363

Description of changes: Nested datatypes are not (yet) allowed in Strata (and are also unsupported by SMT declare_datatype). This adds error checking for such types, including with mutually recursive nesting.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@joscoh joscoh requested a review from a team as a code owner February 2, 2026 20:16
@shigoel shigoel enabled auto-merge February 3, 2026 20:31
Comment thread Strata/DL/Lambda/TypeFactory.lean Outdated
Copy link
Copy Markdown
Contributor

@shigoel shigoel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, with one minor change in the error message wording.

@shigoel shigoel added this pull request to the merge queue Feb 5, 2026
Merged via the queue into main with commit 6effd4d Feb 5, 2026
15 checks passed
@shigoel shigoel deleted the josh/nested-type branch February 5, 2026 20:05
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.

4 participants