[Agda] Defining a module by pattern matching

[Andreas Abel]

What works is

module ModuleArguments {x y : A} (p : x ≡ y) (u : B x) (v : B y) where
   thing' : tr p u ≡ v → u ≡ tr! p v
   thing' h with y | p  | v
   thing' h | .x | refl | v = h

Since matching on p refines y to x, you need to with-abstract also over 
y and v, which mentions y in its type.

What exactly would be your proposal?  That module parameters can be 
refined by unification during pattern matching (as Nisse proposed)?

Cheers,
Andreas

On 15.05.13 10:37 PM, Guillaume Brunerie wrote:
> module Guillaume {A : Set} {B : A → Set} where
>
> open import Relation.Binary.PropositionalEquality
>
> -- This is probably called [subst] or something like that
> tr : {x y : A} (p : x ≡ y) → B x → B y
> tr refl u = u
>
> tr! : {x y : A} (p : x ≡ y) → B y → B x
> tr! refl v = v
>
> module FunctionArguments where
>    thing : {x y : A} (p : x ≡ y) (u : B x) (v : B y) → tr p u ≡ v → u ≡ tr! p v
>    thing refl u v x = x
>
> module ModuleArguments {x y : A} (p : x ≡ y) (u : B x) (v : B y) where
> {- Does not compile
>    thing' : tr p u ≡ v → u ≡ tr! p v
>    thing' rewrite p = {!!}
> -}

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/