diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-09-27 13:11:53 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-09-27 13:11:53 +0200 |
| commit | 1428e4192d61533864a8f163c86272eef4b891cf (patch) | |
| tree | 927de90d713458a7b26693284753627a093d624f /LiftGet.agda | |
| parent | 8546a8812a4fdaf3e3d7a7ba3433894db8b25a14 (diff) | |
| download | bidiragda-1428e4192d61533864a8f163c86272eef4b891cf.tar.gz | |
move definition of get-type to BFF and use it everywhere
Diffstat (limited to 'LiftGet.agda')
| -rw-r--r-- | LiftGet.agda | 8 |
1 files changed, 3 insertions, 5 deletions
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 |