[Agda] heterogeneous equality

[Ulf Norell]

On Mon, Mar 3, 2008 at 4:02 AM, Dan Licata <drl at cs.cmu.edu> wrote:

> Is it possible to define heterogeneous equality in Agda?  I tried:
>
>  data HId {A : Set} : {B : Set} -> A -> B -> Set where
>    HRefl : {a : A} -> HId {A} {A} a a
>
> but I can't figure out how to use it.
>
> E.g., for a context- and object-language-type-indexed expression type
> Tm, I want a congruence for the successor constructor:
>
>  help : { G G' : Ctx} {e : Tm G nat} {e' : Tm G' nat}
>       -> HId e e' -> HId (Succ e) (Succ e')
>  help {G} {.G} {e} {.e} HRefl = ?
>
> But I can't seem to match the input equality with HRefl here:
>
>  G != G' of type .lib.List.List.ListOpenInPrelude.List Tp
>  when checking that the pattern HRefl has type HId e' e0
>
> Any advice?


darcs pull :-)

The unification performed when pattern matching only handled data
constructors (not type constructors), so Tm G nat and Tm G' nat didn't unify
(with G' := G). Fixed now.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080303/2fe733d7/attachment.html