1

I have installed agda using cabal. I have created a file name Trial.agda in the directory /media/arkaghosh/Important5/programs/Agda with the following content inside it

module Trial where

open import Data.Nat

But when I try to compile it using

agda -c Trial.agda

I get the following error

Failed to find source of module Data.Nat in any of the following
locations:
  /media/arkaghosh/Important5/programs/Agda/Data/Nat.agda
  /media/arkaghosh/Important5/programs/Agda/Data/Nat.lagda
  /home/arkaghosh/.cabal/share/x86_64-linux-ghc-7.10.3/Agda-2.6.0.1/lib/prim/Data/Nat.agda
  /home/arkaghosh/.cabal/share/x86_64-linux-ghc-7.10.3/Agda-2.6.0.1/lib/prim/Data/Nat.lagda
when scope checking the declaration
  open import Data.Nat

I have seen this question which is similar to mine Agda: Can't find std-lib when installing with Stack . But I am unable use the answer to solve my problem.

Arka
  • 249
  • 1
  • 8
  • 2
    This is in one of those things which I think Agda documentation is lacking. I had the same problem. Basically, you need to download the standard library and tell "agda" (the executable) where to find it. You can find the standard library here: https://github.com/agda/agda-stdlib and the "instructions" to make the library visible to "agda" are in https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html (you need to create two files inside `~/.agda/`: `defaults` and `libraries`) – helq Jul 21 '20 at 20:56

0 Answers0