We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0b990e0 commit b006b7dCopy full SHA for b006b7d
1 file changed
test/recursive_struct.c
@@ -61,8 +61,9 @@ typedef struct node *list;
61
62
_include_pulse(
63
ghost fn is_list_nil_case (head: $type(node *)) (#l: list Int32.t)
64
- requires is_list head $`p l ** pure (is_null head)
65
- ensures is_list head $`p l ** pure (l == ([] #Int32.t))
+ preserves is_list head $`p l
+ requires pure (is_null head)
66
+ ensures pure (l == [])
67
{
68
match l {
69
Nil -> { () }
0 commit comments