diff options
Diffstat (limited to 'LiftGet.agda')
| -rw-r--r-- | LiftGet.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/LiftGet.agda b/LiftGet.agda index 31a632e..2199aff 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -13,8 +13,8 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨ import FreeTheorems open import Generic using (length-replicate ; subst-cong ; subst-fromList ; subst-subst ; toList-fromList ; toList-subst) -open FreeTheorems.ListList using (get-type ; free-theorem) -open FreeTheorems.VecVec using () renaming (get-type to getV-type) +open FreeTheorems.ListList using (get-type ; free-theorem) renaming (Get to GetL) +open FreeTheorems.VecVec using () renaming (get-type to getV-type ; Get to GetV) getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type getVec-to-getList get = toList ∘ get ∘ fromList |