[Agda] Hello World

[Ben Clifford]

On Aug 8, 2011, at 4:56 AM, Guillaume Yziquel wrote:

> 
>        yziquel at seldon:~/git/agda-learning$ agda -c Main.agda
>        Checking Main (/home/yziquel/git/agda-learning/Main.agda).
>        /home/yziquel/git/agda-learning/Main.agda:11,1-24
>        Failed to find source of module Data.String in any of the following
>        locations:
>          /home/yziquel/git/agda-learning/Data/String.agda
>          /home/yziquel/git/agda-learning/Data/String.lagda
>        when scope checking the declaration
>          open import Data.String

You can use -i to specify more places to look.

Here's an actual command line I use:

agda -c  --universe-polymorphism roman.agda  -i . -i lib/src

It sounds like you want -i . -i /usr/lib/agda-stdlib

Ben