How do I use adt in ensures/requres?

[vkensou]

datatype NullableInt = Some(value: int) | None

method Foo() returns (result: NullableInt)
    ensures result == None
    ensures result is Some(va) && va.value > 0
{
  return Some(1);
}

I define a NullableInt, and return a NullableInt in a method.
But the compiler has a complain:

  |
5 |     ensures result is Some(va) && va.value > 0
  |                           ^
t2.dfy(5,26): Error: this symbol not expected in Dafny

What did I do wrong？

[atomb]

You can write that example something like this:

datatype NullableInt = Some(value: int) | None

method Foo() returns (result: NullableInt)
    ensures result.Some? && result.value > 0
{
  return Some(1);
}

The expression result.Some? evaluates to true if the value of result was constructed with the Some constructor, and the right-hand side of && can assume that the left-hand side is true, so you can directly extract the value field. You could also use a match expression in the ensures clause, but that would be more verbose in this case.

[vkensou]

Thank your answer. It does work!