diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-04 10:52:49 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-04 10:52:49 +0100 |
| commit | 20c176d383e59a0345f7425c5f14679906159a59 (patch) | |
| tree | a2874cac4922670c6d8e8229c24b56a725c11dda /BFF.agda | |
| parent | 257665f2910296c6e87113d2f7a418e1f83b33f6 (diff) | |
| download | bidiragda-20c176d383e59a0345f7425c5f14679906159a59.tar.gz | |
add convenience members to PartialVecVec.Get
Diffstat (limited to 'BFF.agda')
| -rw-r--r-- | BFF.agda | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -38,7 +38,7 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where denumerate = flip lookupV - bff : (G : Get) → ({i : Setoid.Carrier (Get.I G)} → Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i) → Vec Carrier ((Get.gl₂ G) ⟨$⟩ i) → Maybe (Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i))) + bff : (G : Get) → ({i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i))) bff G s v = let s′ = enumerate s t′ = Get.get G s′ g = fromFunc (denumerate s) |