[Agda] Defining a module by pattern matching

[Guillaume Brunerie]

Hi Gergo,

This looks like a good idea but I don’t see how to make it work with
pattern matching on the identity type instead.
The issue is that the identity type is an inductive family, so when
pattern matching against it it will change one of the endpoints (which
is another module argument) so Agda does not like it.

Guillaume

2013/5/15 Dr. ERDI Gergo <gergo at erdi.hu>:
> 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.