Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A combination of forall and invalid is syntax panics the syntax macro #1380

Open
1 task
utaal opened this issue Jan 9, 2025 · 3 comments
Open
1 task

A combination of forall and invalid is syntax panics the syntax macro #1380

utaal opened this issue Jan 9, 2025 · 3 comments

Comments

@utaal
Copy link
Collaborator

utaal commented Jan 9, 2025

Minimized to

        use vstd::seq::*;

        enum Alternative {
            Yes,
            No,
        }

        spec fn is_test_original(s: Seq<Option<Alternative>>) -> bool {
            &&& forall|b:nat| b < s.len() ==> s[b as int] is Some(Alternative::Yes)
        }

        spec fn is_test_minimal(s: Seq<Option<Alternative>>) -> bool {
            &&& forall|b:nat| s[b as int] is Some(Alternative::Yes)
        }

utaal added a commit that referenced this issue Jan 9, 2025
@tjhance

This comment was marked as resolved.

@utaal

This comment was marked as resolved.

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

No branches or pull requests

3 participants
@tjhance @utaal and others