summaryrefslogtreecommitdiff
path: root/Precond.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-03-07 09:16:45 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-03-07 09:16:45 +0100
commitc8f719f7e038ccc720daa488d906bfabf3d27349 (patch)
treea997fe3e9953fcf5a24c1f9a75cce78c822523b6 /Precond.agda
parentd1d4cf511883e1795ee1922a511cc4b0121c5bfa (diff)
downloadbidiragda-c8f719f7e038ccc720daa488d906bfabf3d27349.tar.gz
use allFin rather than tabulate id
Diffstat (limited to 'Precond.agda')
-rw-r--r--Precond.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/Precond.agda b/Precond.agda
index ead2e18..a76fddc 100644
--- a/Precond.agda
+++ b/Precond.agda
@@ -12,7 +12,7 @@ import Category.Functor
open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
-open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList ; tabulate)
+open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘)
import Data.List.All
open import Data.List.Any using (here ; there)