diff options
Diffstat (limited to 'BFF.agda')
| -rw-r--r-- | BFF.agda | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -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 |