From 8e841d13a36cc57300a3fe4eec5305b684212e60 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Tue, 31 Jan 2012 18:32:46 +0100
Subject: replace idrange with enumerate

Looks like uses of idrange would always be passed a length, so move it
inside the definition.
---
 Bidir.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Bidir.agda b/Bidir.agda
index 81f00dd..15a389c 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -93,11 +93,11 @@ lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | Reveal_is_.[_] ir = begin
     ≡⟨ refl ⟩
   map just (x ∷ xs) ∎
 
-idrange : (n : ℕ) → List (Fin n)
-idrange n = toList (tabulate id)
+enumerate : {A : Set} → (l : List A) → List (Fin (length l))
+enumerate l = toList (tabulate id)
 
 bff : ({A : Set} → List A → List A) → ({B : Set} → EqInst B → List B → List B → Maybe (List B))
-bff get eq s v = let s′ = idrange (length s)
+bff get eq s v = let s′ = enumerate s
                      g  = fromFunc (λ f → lookupVec f (fromList s))
                      h  = assoc eq (get s′) v
                      h′ = fmap (flip union g) h
-- 
cgit v1.2.3