add back original bff function before shape updates
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 14 Feb 2014 15:32:20 +0000 (16:32 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 14 Feb 2014 15:32:20 +0000 (16:32 +0100)
BFFPlug.agda

index ef921c2..1d5570c 100644 (file)
@@ -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