Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Monad.Base.Warning
Description
Types related to warnings raised by Agda.
Documentation
data RecordFieldWarning Source #
Constructors
DuplicateFields (List1 (Name, Range)) | Each redundant field comes with a range of associated dead code. |
TooManyFields QName [Name] (List1 (Name, Range)) | Record type, fields not supplied by user, non-fields but supplied. The redundant fields come with a range of associated dead code. |
Instances
EmbPrj RecordFieldWarning Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: RecordFieldWarning -> S Word32 Source # icod_ :: RecordFieldWarning -> S Word32 Source # value :: Word32 -> R RecordFieldWarning Source # | |||||
Generic RecordFieldWarning Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning Associated Types
Methods from :: RecordFieldWarning -> Rep RecordFieldWarning x to :: Rep RecordFieldWarning x -> RecordFieldWarning | |||||
Show RecordFieldWarning Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning Methods showsPrec :: Int -> RecordFieldWarning -> ShowS # show :: RecordFieldWarning -> String # showList :: [RecordFieldWarning] -> ShowS # | |||||
NFData RecordFieldWarning | |||||
Defined in Agda.TypeChecking.Monad.Base Methods rnf :: RecordFieldWarning -> () | |||||
type Rep RecordFieldWarning Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning type Rep RecordFieldWarning = D1 ('MetaData "RecordFieldWarning" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) (C1 ('MetaCons "DuplicateFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, Range)))) :+: C1 ('MetaCons "TooManyFields" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (Name, Range)))))) |
data UselessPublicReason Source #
Instances
EmbPrj UselessPublicReason Source # | |||||
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UselessPublicReason -> S Word32 Source # icod_ :: UselessPublicReason -> S Word32 Source # value :: Word32 -> R UselessPublicReason Source # | |||||
Bounded UselessPublicReason Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning | |||||
Enum UselessPublicReason Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning Methods succ :: UselessPublicReason -> UselessPublicReason pred :: UselessPublicReason -> UselessPublicReason toEnum :: Int -> UselessPublicReason fromEnum :: UselessPublicReason -> Int enumFrom :: UselessPublicReason -> [UselessPublicReason] enumFromThen :: UselessPublicReason -> UselessPublicReason -> [UselessPublicReason] enumFromTo :: UselessPublicReason -> UselessPublicReason -> [UselessPublicReason] enumFromThenTo :: UselessPublicReason -> UselessPublicReason -> UselessPublicReason -> [UselessPublicReason] | |||||
Generic UselessPublicReason Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning Associated Types
Methods from :: UselessPublicReason -> Rep UselessPublicReason x to :: Rep UselessPublicReason x -> UselessPublicReason | |||||
Show UselessPublicReason Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning Methods showsPrec :: Int -> UselessPublicReason -> ShowS # show :: UselessPublicReason -> String # showList :: [UselessPublicReason] -> ShowS # | |||||
NFData UselessPublicReason Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning Methods rnf :: UselessPublicReason -> () | |||||
type Rep UselessPublicReason Source # | |||||
Defined in Agda.TypeChecking.Monad.Base.Warning type Rep UselessPublicReason = D1 ('MetaData "UselessPublicReason" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) ((C1 ('MetaCons "UselessPublicPreamble" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPublicLet" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "UselessPublicNoOpen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UselessPublicAnonymousModule" 'PrefixI 'False) (U1 :: Type -> Type))) |