[ base ] Add anyToFin converting a Vect's Any to its index

idris-lang · Oct 8, 2023 · a9304c0 · a9304c0
1 parent 1256ded
commit a9304c0
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -186,6 +186,9 @@
 
 * Add `zipPropertyWith` to `Data.Vect.Quantifiers.All.All`.
 
+* Add `anyToFin` to `Data.Vect.Quantifiers.Any`,
+  converting the `Any` witness to the index into the corresponding element.
+
 * Implemented `Ord` for `Language.Reflection.TT.Name`, `Language.Reflection.TT.Namespace`
   and `Language.Reflection.TT.UserName`.
 

diff --git a/libs/base/Data/Vect/Quantifiers.idr b/libs/base/Data/Vect/Quantifiers.idr
@@ -61,6 +61,12 @@ namespace Any
   toExists (Here prf)  = Evidence _ prf
   toExists (There prf) = toExists prf
 
+  ||| Get the bounded numeric position of the element satisfying the predicate
+  public export
+  anyToFin : {0 xs : Vect n a} -> Any p xs -> Fin n
+  anyToFin (Here _) = FZ
+  anyToFin (There later) = FS (anyToFin later)
+
 namespace All
   ||| A proof that all elements of a vector satisfy a property. It is a list of
   ||| proofs, corresponding element-wise to the `Vect`.