Multiple lines annotations

[JunmingZhao42]

It seems that multiple lines annotations are not parsed by the transpiler nicely, for example:

fun main() 
{
    // this works
    /*@ requires forall i: Int:: i >= 0 && i < 3 ==> acc(heap[i]) @*/

    // this doesn't work
    /*@ requires forall i: Int:: 
        i >= 0 && i < 3 ==> acc(heap[i]) @*/

    // this works
    /*@ assert forall i: Int:: i >= 0 && i < 3 ==> acc(heap[i]) @*/

    // this doesn't work
    /*@ assert forall i: Int:: 
        i >= 0 && i < 3 ==> acc(heap[i]) @*/
    return 0;
}

The error message is: Variable 'forall' has not been declared which can be a bit misleading.

Might be good to fix, since some annotations can get quite lengthy in some cases. But this is a rather low priority request which would be nice-to-have in the future.

[JunmingZhao42]

Also it seems that the transpiler is not happy with triggers, something like this:

/*@ requires forall i: Int:: {heap[i]} i >= 0 && i < 3 ==> acc(heap[i]) @*/

gives error Shape for 'i' is not known.