diff options
| -rw-r--r-- | BFFPlug.agda | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/BFFPlug.agda b/BFFPlug.agda index ef921c2..1d5570c 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -23,6 +23,9 @@ open DecSetoid A using (Carrier) open GetTypes.VecVec public using (Get) open BFF.VecBFF A public +bffsameshape : (G : Get) → {n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n) +bffsameshape G {n} = bff G n + bffplug : (G : Get) → (ℕ → ℕ → Maybe ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (∃ λ l → Vec Carrier l) bffplug G sput {n} {m} s v with sput n m ... | nothing = nothing |