summaryrefslogtreecommitdiff
path: root/src/full/Agda/Auto/NarrowingSearch.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Auto/NarrowingSearch.hs')
-rw-r--r--src/full/Agda/Auto/NarrowingSearch.hs17
1 files changed, 8 insertions, 9 deletions
diff --git a/src/full/Agda/Auto/NarrowingSearch.hs b/src/full/Agda/Auto/NarrowingSearch.hs
index 8e60324..89cb007 100644
--- a/src/full/Agda/Auto/NarrowingSearch.hs
+++ b/src/full/Agda/Auto/NarrowingSearch.hs
@@ -1,11 +1,10 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
--- {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
module Agda.Auto.NarrowingSearch where
@@ -19,10 +18,10 @@ import Agda.Utils.Impossible
type Prio = Int
class Trav a blk | a -> blk where
- traverse :: Monad m => (forall b . Trav b blk => MM b blk -> m ()) -> a -> m ()
+ trav :: Monad m => (forall b . Trav b blk => MM b blk -> m ()) -> a -> m ()
instance Trav a blk => Trav (MM a blk) blk where
- traverse f me = f me
+ trav f me = f me
data Term blk = forall a . Trav a blk => Term a