From 1428e4192d61533864a8f163c86272eef4b891cf Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Thu, 27 Sep 2012 13:11:53 +0200
Subject: move definition of get-type to BFF and use it everywhere

---
 LiftGet.agda | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'LiftGet.agda')

diff --git a/LiftGet.agda b/LiftGet.agda
index 7731f6b..4c335c9 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -11,11 +11,9 @@ open import Relation.Binary.Core using (_≡_)
 open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
-get-type : Set₁
-get-type = {A : Set} → List A → List A
-
-getV-type : (ℕ → ℕ) → Set₁
-getV-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
+import BFF
+open BFF.ListBFF using (get-type)
+open BFF.VecBFF using () renaming (get-type to getV-type)
 
 getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
 getVec-to-getList get = toList ∘ get ∘ fromList
-- 
cgit v1.2.3