[Agda] Defining a module by pattern matching

[Dr. ERDI Gergo]

On Wed, 15 May 2013, Guillaume Brunerie wrote:

> I have several definitions all starting with the following arguments:
> {x x' : A} {p : x == x'} {u : Π (B x) (C x)} {u' : Π (B x') (C x')}
>
> In order to make the code more readable, I would like to wrap them in
> a section so that I can write the arguments only once.
> The issue is that all those definitions are defined by pattern
> matching on p, so I cannot do it and I need to copy paste the list of
> arguments for each definition which makes the code quite hard to read.

Would something like ths help?

module Guillaume where

open import Data.Bool

-- Here, the Bool is a function argument
module FunctionArguments where
   cond : {A : Set} → Bool → A → A → A
   cond true x y = x
   cond false x y = y

-- Here, the Bool is a module argument, but individual function 
-- definitions still pattern match on it one by one
module ModuleArguments (b : Bool) where
   cond : {A : Set} → A → A → A
   cond x y with b
   cond x y | true = x
   cond x y | false = y

Bye,
 	Gergo

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
Sajnálom, de nem tudok segíteni. Engem csak a szépségem miatt vettek fel.