[Agda] Hello World

[Guillaume Yziquel]

Le Monday 08 Aug 2011 à 08:39:31 (+0200), Ben Clifford a écrit :
> 
> 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

Hmm... I had hoped there were some way to define some kind of default
locations for the libraries.

Thanks, I'll try that right away.

-- 
     Guillaume Yziquel