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

Alan Schmitt alan.schmitt at polytechnique.org
Thu Feb 21 15:47:45 CET 2019


Hello,

I have this very simple specification that creates a type and 
states an
invariant for it.

module Test

use int.Int
use array.Array

type t = { x : array int }
invariant { length x > 0 /\ x[0] > 0 }

end

When I load this in why3, I'm asked to check that the type is 
inhabited.
Is there a way to provide a witness, as why3 is unable to guess 
it?

Thanks,

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/9061e253/attachment.sig>


More information about the Why3-club mailing list