Home
last modified time | relevance | path

Searched refs:UselessInstance (Results 1 – 4 of 4) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Concrete/Definitions/
H A DErrors.hs112 | UselessInstance Range constructor
154 UselessInstance{} -> UselessInstance_
194 UselessInstance{} -> False
230 getRange (UselessInstance r) = r
323 pretty (UselessInstance _) = fsep $
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Serialise/Instances/
H A DErrors.hs166 UselessInstance a -> icodeN 5 UselessInstance a
200 [5, a] -> valuN UselessInstance a
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/Highlighting/
H A DGenerate.hs486 UselessInstance{} -> deadcodeHighlighting w
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Syntax/Concrete/
H A DDefinitions.hs1194 declarationWarning $ UselessInstance r