diff options
| -rw-r--r-- | BFFPlug.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/BFFPlug.agda b/BFFPlug.agda index 12ee980..5c219a5 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -23,7 +23,7 @@ import Examples open DecSetoid A using (Carrier) open GetTypes.PartialVecVec public using (Get) -open BFF.PartialVecBFF A public +open BFF.PartialVecBFF A public using (sbff ; bff) bffsameshape : (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)) bffsameshape G {i} = sbff G i |