[Agda] how to run helloworld in agda

[Andrés Sicard-Ramírez]

On 1 January 2016 at 00:39, Mandy Martino <tesleft at hotmail.com> wrote:
> /home/martin/hilbertreborn/hello.agda:14,1-19
> Repeated variables in pattern: refl1
> when scope checking the left-hand side trans1 refl1 refl1 in the
> definition of trans1
>
> trans1 : ∀ {X} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
> trans1 refl1 refl1 = refl1
>

The above error is similar to the error in the following Haskell code:

  foo :: Int -> Int -> Int
  foo a a = a

-- 
Andrés