summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Info.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Info.hs')
-rw-r--r--src/full/Agda/Syntax/Info.hs10
1 files changed, 6 insertions, 4 deletions
diff --git a/src/full/Agda/Syntax/Info.hs b/src/full/Agda/Syntax/Info.hs
index 53f990f..abc766e 100644
--- a/src/full/Agda/Syntax/Info.hs
+++ b/src/full/Agda/Syntax/Info.hs
@@ -1,7 +1,5 @@
{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-| An info object contains additional information about a piece of abstract
@@ -169,6 +167,10 @@ data MutualInfo = MutualInfo
}
deriving (Typeable, Show, Eq)
+-- | Default value for 'MutualInfo'.
+instance Null MutualInfo where
+ empty = MutualInfo TerminationCheck True noRange
+
instance HasRange MutualInfo where
getRange = mutualRange
@@ -203,7 +205,7 @@ patNoRange = PatRange noRange
-- | Constructor pattern info.
data ConPatInfo = ConPatInfo
- { patOrigin :: ConPOrigin
+ { patOrigin :: ConOrigin
-- ^ Does this pattern come form the eta-expansion of an implicit pattern?
--- Or from a user written constructor or record pattern?
, patInfo :: PatInfo
@@ -211,7 +213,7 @@ data ConPatInfo = ConPatInfo
deriving (Typeable, Eq)
instance Show ConPatInfo where
- show (ConPatInfo po i) = applyWhen (po == ConPImplicit) ("implicit " ++) $ show i
+ show (ConPatInfo po i) = applyWhen (po == ConOSystem) ("implicit " ++) $ show i
instance HasRange ConPatInfo where
getRange = getRange . patInfo