[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