Is there an example that uses a while loop to iterate over the elements of
a list? I tried:
while (not(!rdy = Nil))
do
variant { !rdy }
match !rdy with
Nil -> ()
| Cons t ts ->
rdy := ts;
end;
done
but at the call site of the function that contains this code,
On Thu, 29 Mar 2018, Jean-Christophe Filliatre wrote:
> Hi Julia,
>
> > but at the call site of the function that contains this code, it complains
> > that:
> >
> > warning: this expression may diverge, which is not stated in the
> > specification
> >
> > Can I just ignore the warning?
>
> If
On Thu, 29 Mar 2018, Jean-Christophe Filliatre wrote:
> Hi Julia,
>
> > but at the call site of the function that contains this code, it complains
> > that:
> >
> > warning: this expression may diverge, which is not stated in the
> > specification
> >
> > Can I just ignore the warning?
>
> If
