[Why3-club] matrix import
julia.lawall at lip6.fr
Mon Jul 2 12:43:43 CEST 2018
On Mon, 2 Jul 2018, Andrei Paskevich wrote:
> Hi Julia,
> you simply write "use array.Array" and "use matrix.Matrix" — the import will
> be done by default. You wirte "use ... as" when you _don't_ want import.
> And, of course, you still can write "use import array.Array as A" if you
> want to name the scope "A" _and_ to import it, too.
>From what you say it seems like what I have should work. But it does not.
I can try to make a small example.
> On 2 July 2018 at 12:04, Julia Lawall <julia.lawall at lip6.fr> wrote:
> I am trying to get my 0.88 code to work with why3 1.0. I have
> use import array.Array as A
> use import matrix.Matrix as MM
> According to my understanding, the imports are no longer
> needed. I tried:
> use array.Array as A
> use matrix.Matrix as MM
> but then it doesn't recognize the type matrix.
> With the imports it doesn't recognize MM.set. What should be
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club