[Agda] Installing standard and plfa libraries

[Michel Levy]

Excuse me. I have already found a solution to my problem :

1) Create the missing file "standard-library.agda-lib in the directory
of the standard library

2) Create the directory "my_home/.agda. In the file libraries write the
path to the two files agda-lib. In the defauts file, write plfa and
standard-library.

Le 12/04/2020 à 14:24, Michel Levy a écrit :
> I'm trying to write all the PLFA exercises.  But I have a problem
> installing the pfla library.
> More exactly the standard library is usable without "my home/.agda"
> directory. This library doesn't have a "standard-library.agda-lib" file.
> When I create a ".agda" directory with only the plfa library, I lose
> access to the standard library.
> This library doesn't have a "standard-library.agda-lib" file.
> When I create a "my home/.agda" directory with only the plfa library, I
> lose access to the standard library.
> What do I have to do to get both standard and plfa libraries?
>
> PS : my agda version is 2.5.3 installed with the Ubuntu packages.
>
-- 
courriel : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr