[Agda] Two antagonistic definitions

[Martin Escardo]

The following lectures notes discuss this kind of problem and how to 
address it:

http://www.cs.bham.ac.uk/~mhe/dependent-equality-lecture/DependentEquality.html

If after reading this you need further help, please ask and I'll be 
happy to discuss.

Best,
Martin


On 11/04/2019 15:48, pierre.lescanne at ens-lyon.fr wrote:
> Here is my problem. I set it in the Vec data structure, since it is a 
> well known.
> 
> Assume that I want to define both ++ and another operation ++ʳ
> 
> 
> _++_ : ∀{A : Set}{n m : ℕ} → Vec A n → Vec A m → Vec A (n + m)
> [] ++ v = v
> (x ∷ v₁) ++ v₂ = x ∷ (v₁ ++ v₂)
> 
> _++ʳ_ : ∀{A : Set}{n m : ℕ} → Vec A n → Vec A m → Vec A (n + m)
> v ++ʳ [] = v
> v₁ ++ʳ (x ∷ v₂) = (v₁ ∷ʳ x) ++ʳ v₂
> 
> Agda does want to accept the second definition or the first if I use Vec 
> A (m + n) instead.   How should I proceed ?
> 
> Pierre Lescanne
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe