[Agda] how to run helloworld in agda

[Sergei Meshveliani]

On Sat, 2015-12-19 at 18:20 +0800, Mandy Martino wrote:
> Hi  Andres,
> 
> 
> is there an  example to use  function  in Algebra folder
> and import  Algebra?
> [..]

----------------------------------------------------------
module TT where

open import Algebra using (Semigroup; module Semigroup)

square : ∀ {c l} → (H : Semigroup c l) → 
                        let open Semigroup H using (Carrier)
                        in
                        Carrier → Carrier
square H x =  x ∙ x
              where
              open Semigroup H using (_∙_)

-- Another usage:
--
module _ {c l} (H : Semigroup c l)
  where
  open Semigroup H using (_∙_) renaming	(Carrier to C)

  sq : C → C
  sq x = x ∙ x

  -- Other functions can be added to this module:  
  -- foo : C  → C → C
  -- foo = ...
-------------------------------------------------------------


Type checking:

     agda -i . -i $agdaStLib TT.agda

where  /home/mechvel/agda/stLib/dec18-2015/src/ 

is the path to the the Standard library .../src  folder.