[Why3-club] Problem with type definition

Benjamin Gregoire Benjamin.Gregoire at inria.fr
Thu Feb 9 16:15:55 CET 2012


Sorry the error message come with the following type definition:

     type t = ((int,int), (int,int))

The other part of my previous message is correct.
  B

On 02/09/2012 04:12 PM, 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