[Agda] how to run helloworld in agda

[Andrés Sicard-Ramírez]

On 19 December 2015 at 07:01, Mandy Martino <tesleft at hotmail.com> wrote:
> succeed to run an example,  but  got error  +  not  in scope  when follow a
> web  site,
>
> open import Algebra.Structures as A using (IsCommutativeMonoid)
> open import Data.Nat.Properties using (isCommutativeSemiring)
>

Missing modules:

open import Data.Nat.Base
open import Relation.Binary.PropositionalEquality

Please report this error to the author of the Agda tutorial.

-- 
Andrés