replace idrange with enumerate
authorHelmut Grohne <helmut@subdivi.de>
Tue, 31 Jan 2012 17:32:46 +0000 (18:32 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Tue, 31 Jan 2012 17:32:46 +0000 (18:32 +0100)
Looks like uses of idrange would always be passed a length, so move it
inside the definition.

Bidir.agda

index 81f00dd..15a389c 100644 (file)
@@ -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