Skip to content

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

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.

Sign up for GitHub

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

Jump to bottom

Replace fully axiomatic Seq with a model #986

Closed
tchajed opened this issue Feb 15, 2024 · 0 comments · May be fixed by #988
Closed

Replace fully axiomatic Seq with a model #986

tchajed opened this issue Feb 15, 2024 · 0 comments · May be fixed by #988

Comments

@tchajed
Copy link
Collaborator

tchajed commented Feb 15, 2024

The following datatype should be adequate as a model for all of the sequence axioms:

#[verifier::accept_recursive_types(A)]
pub enum Seq<A> {
    Nil,
    Cons(A, Box<Seq<A>>),
}

We should use this as the model and prove the current set of axioms against it.
@tchajed tchajed mentioned this issue Feb 15, 2024
Draft
@verus-lang verus-lang locked and limited conversation to collaborators Feb 23, 2024
@utaal-b utaal-b converted this issue into discussion #1011 Feb 23, 2024

This issue was moved to a discussion.

You can continue the conversation there. Go to discussion →

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Change Seq to an enum and verify its axioms verus-lang/verus
1 participant
@tchajed