diff options
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -8,7 +8,7 @@ open import Data.Fin using (Fin) import Level import Category.Monad import Category.Functor -open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq) +open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just ; just-injective) renaming (setoid to MaybeSetoid ; Eq to MaybeEq) import Data.Maybe.Categorical open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_) @@ -29,7 +29,7 @@ open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped) open import Instances using (MaybeFunctor ; ShapedISetoid) import GetTypes open GetTypes.PartialShapeShape using (Get ; module Get) -open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective) +open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid) open import FinMap import CheckInsert open CheckInsert A |