From c63ff4179147ab237afe7d21d9e3740737c9b942 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Jan 2014 09:02:06 +0100 Subject: 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. --- BFF.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'BFF.agda') diff --git a/BFF.agda b/BFF.agda index 61eeefd..79f3b3d 100644 --- a/BFF.agda +++ b/BFF.agda @@ -19,7 +19,7 @@ import CheckInsert import FreeTheorems module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where - open FreeTheorems.VecVec public using (get-type) + open FreeTheorems.VecVec public using (Get) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) open CheckInsert A @@ -33,9 +33,9 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV - bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) - bff get s v = let s′ = enumerate s - t′ = get s′ + bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)) + bff G s v = let s′ = enumerate s + t′ = Get.get G s′ g = fromFunc (denumerate s) g′ = delete-many t′ g h = assoc t′ v -- cgit v1.2.3