From d8ed3c5d8bb02c626b3d263ed9d6a4bcb5836ae0 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Tue, 9 Jun 2015 16:33:31 +0200 Subject: drop barred members from GetTypes These became duplicates of their non-barred counterparts. --- GetTypes.agda | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'GetTypes.agda') diff --git a/GetTypes.agda b/GetTypes.agda index 286b9aa..83f6845 100644 --- a/GetTypes.agda +++ b/GetTypes.agda @@ -29,14 +29,8 @@ module PartialVecVec where I : Set gl₁ : I → ℕ gl₂ : I → ℕ - - |I| = I - |gl₁| = gl₁ - |gl₂| = gl₂ - - field - get : {A : Set} {i : |I|} → Vec A (|gl₁| i) → Vec A (|gl₂| i) - free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get + get : {A : Set} {i : I} → Vec A (gl₁ i) → Vec A (gl₂ i) + free-theorem : {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get VecVec-to-PartialVecVec G = record @@ -62,16 +56,12 @@ module PartialShapeShape where gl₁ : I → SourceShape gl₂ : I → ViewShape - |I| = I - |gl₁| = gl₁ - |gl₂| = gl₂ - open Shaped SourceShapeT using () renaming (fmap to fmapS) open Shaped ViewShapeT using () renaming (fmap to fmapV) field - get : {A : Set} {i : |I|} → SourceContainer A (|gl₁| i) → ViewContainer A (|gl₂| i) - free-theorem : {α β : Set} → (f : α → β) → {i : |I|} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get + get : {A : Set} {i : I} → SourceContainer A (gl₁ i) → ViewContainer A (gl₂ i) + free-theorem : {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get open Shaped SourceShapeT public using () renaming (fmap to fmapS) open Shaped ViewShapeT public using () renaming (fmap to fmapV) -- cgit v1.2.3