[Why3-club] request for comments

David MENTRE dmentre at linux-france.org
Sun Sep 30 19:08:42 CEST 2012


Hello Andrei,

I am not a heavy user of Why3. Anyway, my 2 cents.

2012/9/20 Andrei Paskevich <andrei at tertium.org>:
> val rec length (l : list int) : int
>   ensures { result = length l }
>   variant { l }
> = match l with ...

I find above form clearer.

[...]
> I think, we can require braces in the effect clauses.

I think it would be better (symmetry, more visual delimitation).

Best regards,
david



More information about the Why3-club mailing list