Python plugin: add extensional definition of lists in the logic
Currently, the micro Python input format has syntax for extensional definition of lists in Python code ([e1, e2, ..., en]
) but not in logical annotations.
In code, an extensional list [e1, e2, ..., en]
is translated to WhyML as follows:
let s = make n e1 in
s[1] <- e2;
...
s[n-1] <- en;
s
This is related to having array/sequence literals in Why3.