[Agda] lost in modules

Michel Levy michel.levy.imag at free.fr
Fri May 1 13:55:41 CEST 2020


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 :

/home/michel/Agda/PLFA-LIB/plfa.agda-lib
/home/michel/agda-stdlib-1.3/standard-library.agda-lib

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 ? 

-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200501/db9810ef/attachment.html>


More information about the Agda mailing list