diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-09-26 13:02:25 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-09-26 13:02:25 +0200 |
| commit | f9fc1aba9386216a6a01ba17d85fcae71756d928 (patch) | |
| tree | 723a6b00a3baa12e618839f1e0de5f852aff1b99 | |
| parent | 51dad2ec627203822e1879e3d58ae5331e58d414 (diff) | |
| download | bidiragda-f9fc1aba9386216a6a01ba17d85fcae71756d928.tar.gz | |
resolve ambiguity in BFFPlug
Fixes compilation with Agda 2.4.2.
| -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 |