[Why3-club] Problem with type definition

Benjamin Gregoire Benjamin.Gregoire at inria.fr
Thu Feb 9 16:12:00 CET 2012


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





More information about the Why3-club mailing list