[Agda] Unification failure when using Pointwise-length

[Apostolis Xekoukoulotakis]

You can try this function :
```
failed : ∀ {Σ' Σ t} → t ∈ Σ → Σ' ⊑ₕ Σ → Type
failed {Σ'} mem prec with length Σ' | ⊑ₕ-length prec
failed {Σ'} mem prec | _ | refl = {!!}
```

On Tue, Jan 8, 2019 at 5:48 AM Deyaaeldeen <diaa6510 at gmail.com> wrote:

> Hello,
>
> I want to use the fact that two lists have the same length if they are
> Pointwise, witnessed by the Pointwise-length function. However, Agda
> complains about the constructor refl at line 51 in the
> self-contained agda file located here:
> https://gist.github.com/deyaaeldeen/1fbc17082f6af8c2d3e45849abacdd51
>
> Your input is much appreciated.
>
> Deyaa
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190108/a42b898a/attachment.html>