Hello, in the library of sequences, several definitions use a while loop that is never executed. For instance, the function set <> (s:seq <http://why3.lri.fr/stdlib/seq.html#seq_14> 'a) (i:int) (v:'a) : seq <http://why3.lri.fr/stdlib/seq.html#seq_14> 'a starts with while false do variant { 0 } () done; Are these loops mandatory ?
Sandrine
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
