add index function for Data.List.Quantifiers.All
commit9baca94b8b40f4ee69479e5a9a329a7a8d31a2f5
authorAlex Gryzlov <skyrodent@gmail.com>
dateTue 10 Dec 2019, 01:22 (7 years ago)
parent4d8d85d
libs/base/Data/List/Quantifiers.idr+5
@@ -75,3 +75,8 @@ all d (x::xs) with (d x)
7575 case all d xs of
7676 Yes prf' => Yes (prf :: prf')
7777 No prf' => No (notAllThere prf')
78+
79+||| Given a proof of membership for some element, extract the property proof for it
80+indexAll : Elem x xs -> All p xs -> p x
81+indexAll Here (p::_ ) = p
82+indexAll (There e) ( _::ps) = indexAll e ps