lookup for List and FinData. (#749)

Co-authored-by: Andreas Nuyts <andreas.nuyts@vub.ac.be>
agda · Apr 4, 2022 · fa0fa06 · fa0fa06
1 parent 2315a8c
commit fa0fa06
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/Cubical/Data/List/FinData.agda b/Cubical/Data/List/FinData.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.List.FinData where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.List
+open import Cubical.Data.FinData
+
+variable
+  ℓ : Level
+  A : Type ℓ
+
+-- copy-paste from agda-stdlib
+lookup : ∀ (xs : List A) → Fin (length xs) → A
+lookup (x ∷ xs) zero    = x
+lookup (x ∷ xs) (suc i) = lookup xs i