[Agda] Another Data.List.Any - Is it possible?
Dmytro Starosud
d.starosud at gmail.com
Tue Jan 29 21:22:09 CET 2013
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
More information about the Agda
mailing list