[Why3-club] matrix import

Julia Lawall julia.lawall at lip6.fr
Mon Jul 2 12:15:08 CEST 2018



On Mon, 2 Jul 2018, Ralf Treinen wrote:

> Hi,
>
> On Mon, Jul 02, 2018 at 12:04:14PM +0200, Julia Lawall wrote:
>
> > 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?
>
> the stdlib has changed location. In my case I had to remove my old
> ~/.why3.conf et rerun "why3 config".

I did that already.  I have:

loadpath = "/home/jll/.opam/default/share/why3/stdlib"

This directory exists and contains the file matrix.mlw.  That file defines
set.

julia

>
> -Ralf.
> --
> Ralf Treinen
> Institut de Recherche en Informatique Fondamentale
> Équipe Preuves, Programmes et Systèmes
> Université Paris Diderot, Paris, France.
> http://www.irif.fr/~treinen/
> _______________________________________________
> 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