{-# OPTIONS --safe --without-K #-}
 
module Meta.Prelude where
 
open import Level renaming (_⊔_ to _⊔ˡ_; suc to sucˡ; zero to zeroˡ) public
open import Function public
 
open import Data.Bool hiding (_≟_; _≤_; _≤?_; _<_; _<?_) public
open import Data.Empty public
open import Data.List hiding (align; alignWith; fromMaybe; map; zip; zipWith) public
open import Data.Maybe hiding (_>>=_; ap; align; alignWith; fromMaybe; map; zip; zipWith) public
open import Data.Unit hiding (_≟_) public
open import Data.Sum hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap) public
open import Data.Product hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip; zipWith) public
open import Data.Nat hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_) public
open import Data.String using (String; _<+>_) public
 
open import Relation.Binary.PropositionalEquality hiding (preorder; setoid; [_]; module ≡-Reasoning; decSetoid) public
 
lookupᵇ : {A B : Set} → (A → A → Bool) → List (A × B) → A → Maybe B
lookupᵇ f [] n = nothing
lookupᵇ f ((k , v) ∷ l) n = if f k n then just v else lookupᵇ f l n
 
open import Data.Fin
open import Data.List
 
zipWithIndex : {A B : Set} → (ℕ → A → B) → List A → List B
zipWithIndex f l = zipWith f (upTo $ length l) l
 
enumerate : {A : Set} → List A → List (ℕ × A)
enumerate = zipWithIndex _,_