We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
Given this definition:
struct Node<V> { v: V, next: Option<Box<Node<V>>>, }
This works:
impl<V> Node<V> { #[ghost] fn len_logic(self: Node<V>) -> Int { { let Node { v: _, next } = self; 1 + match next { Some(next) => next.len_logic(), None => 0, } } } }
While this fails with "Cannot prove termination for len_logic":
impl<V> Node<V> { #[ghost] fn len_logic(self: Node<V>) -> Int { { 1 + match self.next { Some(next) => next.len_logic(), None => 0, } } } }
Note that the only difference is how next is accessed.
next
The text was updated successfully, but these errors were encountered:
xldenis
No branches or pull requests
Given this definition:
This works:
While this fails with "Cannot prove termination for len_logic":
Note that the only difference is how
next
is accessed.The text was updated successfully, but these errors were encountered: