[Why3-club] matrix import

Julia Lawall julia.lawall at lip6.fr
Mon Jul 2 12:59:49 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.

OK, I think my system is set up in an incoherent way at themoment.  That
is probably the source of the problem.

julia

>
> Best,
> Andrei
>
> On 2 July 2018 at 12:04, Julia Lawall <julia.lawall at lip6.fr> wrote:
>       Hello,
>
>       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
>       done
>       instead?
>
>       julia
>       _______________________________________________
>       Why3-club mailing list
>       Why3-club at lists.gforge.inria.fr
>       https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
>
>


More information about the Why3-club mailing list