Re: [Why3-club] Pb. with the matrix library

2014-01-25 Thread David MENTRÉ
Hello Andrei, 2014-01-24 13:59, Andrei Paskevich: On 24 January 2014 11:02, Sandrine Blazysandrine.bl...@irisa.fr wrote: [...] File maze.mlw, line 5, characters 2-26: Symbol set is already defined in the current scope [...] Thus, in the context of your module Maze, the line use import

[Why3-club] Pb. with the matrix library

2014-01-24 Thread Sandrine Blazy
Hi, I don't understand the errors I've got when I write the following module. File maze.mlw, line 5, characters 2-26: Symbol set is already defined in the current scope module Maze use import int.Int use import bool.Bool use import matrix.Matrix as M use import matrix.Syntax type

Re: [Why3-club] Pb. with the matrix library

2014-01-24 Thread Andrei Paskevich
On 24 January 2014 11:02, Sandrine Blazy sandrine.bl...@irisa.fr wrote: Hi, I don't understand the errors I've got when I write the following module. File maze.mlw, line 5, characters 2-26: Symbol set is already defined in the current scope module Maze use import int.Int use import