From c8f719f7e038ccc720daa488d906bfabf3d27349 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Fri, 7 Mar 2014 09:16:45 +0100 Subject: use allFin rather than tabulate id --- BFF.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'BFF.agda') diff --git a/BFF.agda b/BFF.agda index 9fc0afe..2ce24db 100644 --- a/BFF.agda +++ b/BFF.agda @@ -9,8 +9,8 @@ open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List ; [] ; _∷_ ; map ; length) -open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) -open import Function using (id ; _∘_ ; flip) +open import Data.Vec using (Vec ; toList ; fromList ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) +open import Function using (_∘_ ; flip) open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) open import FinMap @@ -28,10 +28,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where assoc (i ∷V is) (b ∷V bs) = (assoc is bs) >>= (checkInsert i b) enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n - enumerate _ = tabulate id + enumerate {n} _ = allFin n enumeratel : (n : ℕ) → Vec (Fin n) n - enumeratel _ = tabulate id + enumeratel = allFin denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV -- cgit v1.2.3