[Why3-club] strange loops in the sequence library

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Tue Feb 26 16:05:10 CET 2019


This is (a hack) to ensure that the definition is not translated to the
logic side.

--
Jean-Christophe

On 2/26/19 9:40 AM, Sandrine Blazy wrote:
> 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 at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> 


More information about the Why3-club mailing list