diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-14 16:32:20 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-14 16:32:20 +0100 |
| commit | 0ff83361e08eec6d6a5ab9a44f35b0b8590d2031 (patch) | |
| tree | 02c8c43dd8aaf494bb9d74ce3677bd0bfc0941bc /BFFPlug.agda | |
| parent | e545ac3a23792e1905bf1b4aedb1f96ebb5a9e90 (diff) | |
| download | bidiragda-0ff83361e08eec6d6a5ab9a44f35b0b8590d2031.tar.gz | |
add back original bff function before shape updates
Diffstat (limited to 'BFFPlug.agda')
| -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 |