<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<pre>This morning, I have loaded (from GitHub) the standard library with the version 1.3.
I have change .agda/libraries to the new version. That is my .agda/libraries file :</pre>
<pre>/home/michel/Agda/PLFA-LIB/plfa.agda-lib
/home/michel/agda-stdlib-1.3/standard-library.agda-lib
</pre>
<pre>But when I retry to load a file "relationsPLFA.agda", agda, on a command "open import Data.nat" is also searching (twice) in the old
version of the standard libray and give the error :
Ambiguous module name. The module name Data.Nat could refer to any
of the following files:
/home/michel/agda-stdlib-1.3/src/Data/Nat.agda
/usr/share/agda-stdlib/Data/Nat.agda
/usr/share/agda-stdlib/Data/Nat.agda
when scope checking the declaration
open import Data.Nat using (ℕ; zero; suc; _+_)
What should I do to avoid this search in the old library ?
</pre>
<div class="moz-signature">-- <br>
courriel : <a class="moz-txt-link-abbreviated"
href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</a>
<br>
mobile : 06 59 13 42 53<br>
web : michel.levy.imag.free.fr </div>
</body>
</html>