[Agda] stdlib for practical programming

[Wolfram Kahl]

On Thu, Sep 26, 2013 at 10:44:14PM +0300, Dmytro Starosud wrote:
> e.g. I would like following:
> 
> open import Prelude -- Prelude is this wanted "some library"
> {- many useful stuff here -}
> 
> instead of:
> 
> open import Level renaming (zero to zeroL; suc to sucL; \lub to \lubL)
> open import Data.Nat renaming (zero to zeroN; suc to sucN; \lub to \lubN; ...)
> open import Data.List renaming (map to mapL; foldr to foldrL; ...)
> open import Data.Vector renaming (map to mapV; foldr to foldrV; ...)
> open import Data.Product renaming (map to mapP; ...)


It gets better if you can adapt to qualified names,
and get used to the constructor overloading that is legal in Agda:

open import Level                using (Level)              -- Use Level.zero, Level.suc
open import Data.Nat    as Nat   using (Nat ; zero ; suc)   -- Use Nat.+ as infix operator
open import Data.Fin    as Fin   using (Fin ; zero ; suc)   -- Use Fin.+ as infix operator
open import Data.List   as List  using (List ; [] ; _::_)   -- Use List.map
open import Data.Vec    as Vec   using (Vec ; [] ; _::_)    -- Use Vec.map

I find fine-grained import control useful for more precise dependency
awareness at module read time...


Wolfram