[Why3-club] matrix import

Andrei Paskevich andrei.paskevich at lri.fr
Mon Jul 2 12:32:04 CEST 2018


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.

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20180702/12a408d2/attachment.html>


More information about the Why3-club mailing list