[Why3-club] matrix import
julia.lawall at lip6.fr
Mon Jul 2 12:15:08 CEST 2018
On Mon, 2 Jul 2018, Ralf Treinen wrote:
> 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
> Ralf Treinen
> Institut de Recherche en Informatique Fondamentale
> Équipe Preuves, Programmes et Systèmes
> Université Paris Diderot, Paris, France.
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club