Agda-2.8.0: A dependently typed functional programming language and proof assistant

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

Instances details

EmbPrj RecordFieldWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: RecordFieldWarning -> S Word32 Source # icod_ :: RecordFieldWarning -> S Word32 Source # value :: Word32 -> R RecordFieldWarning Source #
NFData RecordFieldWarning Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods rnf :: RecordFieldWarning -> () Source #
Generic RecordFieldWarning Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

Associated Types

type Rep RecordFieldWarning |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep RecordFieldWarning = D1 ('MetaData "RecordFieldWarning" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))

Methods

from :: RecordFieldWarning -> Rep RecordFieldWarning x Source #

to :: Rep RecordFieldWarning x -> RecordFieldWarning Source #

Show RecordFieldWarning Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Warning Methods showsPrec :: Int -> RecordFieldWarning -> ShowS Source # show :: RecordFieldWarning -> String Source # showList :: [RecordFieldWarning] -> ShowS Source #
type Rep RecordFieldWarning Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep RecordFieldWarning = D1 ('MetaData "RecordFieldWarning" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 #

Constructors

UselessPublicPreamble |
UselessPublicLet |
UselessPublicNoOpen |
UselessPublicAnonymousModule |

#### Instances

Instances details

EmbPrj UselessPublicReason Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UselessPublicReason -> S Word32 Source # icod_ :: UselessPublicReason -> S Word32 Source # value :: Word32 -> R UselessPublicReason Source #
NFData UselessPublicReason Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Warning Methods rnf :: UselessPublicReason -> () Source #
Bounded UselessPublicReason Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Warning Methods minBound :: UselessPublicReason Source # maxBound :: UselessPublicReason Source #
Enum UselessPublicReason Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

Methods

succ :: UselessPublicReason -> UselessPublicReason Source #

pred :: UselessPublicReason -> UselessPublicReason Source #

toEnum :: Int -> UselessPublicReason Source #

fromEnum :: UselessPublicReason -> Int Source #

enumFrom :: UselessPublicReason -> [UselessPublicReason] Source #

enumFromThen :: UselessPublicReason -> UselessPublicReason -> [UselessPublicReason] Source #

enumFromTo :: UselessPublicReason -> UselessPublicReason -> [UselessPublicReason] Source #

enumFromThenTo :: UselessPublicReason -> UselessPublicReason -> UselessPublicReason -> [UselessPublicReason] Source #

Generic UselessPublicReason Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

Associated Types

type Rep UselessPublicReason |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep UselessPublicReason = D1 ('MetaData "UselessPublicReason" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: UselessPublicReason -> Rep UselessPublicReason x Source #

to :: Rep UselessPublicReason x -> UselessPublicReason Source #

Show UselessPublicReason Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base.Warning Methods showsPrec :: Int -> UselessPublicReason -> ShowS Source # show :: UselessPublicReason -> String Source # showList :: [UselessPublicReason] -> ShowS Source #
type Rep UselessPublicReason Source # |

Instance details

Defined in Agda.TypeChecking.Monad.Base.Warning

type Rep UselessPublicReason = D1 ('MetaData "UselessPublicReason" "Agda.TypeChecking.Monad.Base.Warning" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))