[Why3-club] Problem with type definition

Andrei Paskevich andrei at tertium.org
Fri Feb 10 09:08:52 CET 2012


Hello,

this is a bug which we'll fix asap. Thanks for reporting.

Best,
Andrei

On Thu, 09 Feb 2012 at 16:12:00 (+0100), Benjamin Gregoire wrote:
> Hi,
>    When I try to defined the following theory
> 
> theory Toto
>   use import int.Int
>   type t = (int,int)
> end
> 
> I got the following error:
> File "why3-0.71/test/list1.why", line 4, characters 0-3:
> Cannot construct a value of type t
> 
> When I try to build a task containing the declaration of the type t
> (using the api)
> I got the following exception:
>   Decl.NonFoundedTypeDecl(t)
> 
> Do you have some explanation.
>   Best,
>     Benjamin
> 
> 
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club





More information about the Why3-club mailing list