diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-30 09:02:06 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-30 09:02:06 +0100 |
| commit | c63ff4179147ab237afe7d21d9e3740737c9b942 (patch) | |
| tree | 0fb4defb70302a2cba13b6f75f82fac39f15514e /LiftGet.agda | |
| parent | 26e2fea33aae257440e5571fb3f7e784938403e0 (diff) | |
| download | bidiragda-c63ff4179147ab237afe7d21d9e3740737c9b942.tar.gz | |
pass get functions as records
This allows passing both getlen and get as a single parameter. It also
allows to make the free theorem a prerequisite instead of a postulate.
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 |