Merge pull request #4790 from clayrat/patch-17
add index function for Data.List.Quantifiers.All
commit94a6326a10da897c3e8cfb9690fb3b49efda58ba
authorNiklas Larsson <metaniklas@gmail.com>
dateSat 21 Dec 2019, 13:36 (7 years ago)
parent7690efb9baca94
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