On 2020-05-30 22:05, Michel Levy wrote: > The standard library seems badly installed: The commands you used do not install the standard library. You can download the library separately: https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary -- /NAD