[Agda] Another Data.List.Any - Is it possible?

[Dmytro Starosud]

Hello everyone!

In stdlib-0.6 we have:
data Any {a p} {A : Set a} (P : A → Set p) : List A → Set (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

When I didn't know about it, I tried to do it in the following way:
data Any {A : Set} (P : A → Set) : List A → Set where
  exact : ∀ {x} l r → P x → Any P (l ++ x ∷ r)

For the reasoning I needed a function:
AnyP[h∷t]⇒Ph⊎AnyPt : {A : Set} {P : A → Set} {h : A} {t : List A} → Any P
(h ∷ t) → P h ⊎ Any P t
AnyP[h∷t]⇒Ph⊎AnyPt .{h = x} .{t = r} (exact {x = x} [] r p) = _
AnyP[h∷t]⇒Ph⊎AnyPt .{h = l} .{t = ls ++ x ∷ r} (exact {x = x} (l ∷ ls) r p)
= _

But I got stuck in implementation.
Could you please help me with it?
*I don't need such "Any" type, but I am interested whether it is possible
to do it. And if it is not possible, then why?
**I think here some information might be missed like in square function:
having x^2 we don't know whether x is positive or negative.

Thank you,
Dmytro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130129/bd84e6be/attachment.html