[Why3-club] how to prove a type is inhabited?

Alan Schmitt alan.schmitt at polytechnique.org
Thu Feb 21 15:56:19 CET 2019


On 2019-02-21 15:51, Raphael Rieu-Helft 
<raphael.rieu-helft at lri.fr> writes:

> Use the keyword `by`:
>
> type t = { x = array int } invariant { length x > 0 /\ x[0] > 0 
> } by { x
> = Array.make 1 1 }

Thanks, that works great on my much more complex example.

Alan
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190221/e8e0e498/attachment.sig>


More information about the Why3-club mailing list