(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(1 36 (comment) t) '(37 39 (comment) t) '(40 92 (comment) t) '(93 135 (comment) t) '(137 141 (keyword) t) '(142 148 (keyword) t) '(177 178 (symbol) t) '(183 184 (symbol) t) '(203 204 (symbol) t) '(205 206 (number) t) '(217 218 (symbol) t) '(223 224 (symbol) t) '(225 226 (symbol) t) '(231 232 (symbol) t) '(243 244 (symbol) t) '(255 256 (symbol) t) '(261 262 (symbol) t) '(281 282 (symbol) t) '(301 302 (symbol) t) '(319 320 (symbol) t) '(334 338 (keyword) t) '(350 351 (symbol) t) '(356 361 (keyword) t) '(368 369 (symbol) t) '(370 371 (symbol) t) '(382 383 (symbol) t) '(387 388 (symbol) t) '(389 390 (symbol) t) '(412 413 (symbol) t) '(427 428 (symbol) t) '(434 497 (comment) t))
(agda2-highlight-add-annotations 'nil '(149 165 (module) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 1)) '(167 176 (function) nil nil ("Issue3417.agda" . 167)) '(179 182 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)) '(185 188 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)) '(189 198 (function) nil nil ("Issue3417.agda" . 167)) '(199 202 (bound) nil nil ("Issue3417.agda" . 199)) '(207 216 (function) nil nil ("Issue3417.agda" . 167)) '(218 221 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 208)) '(222 223 (bound) nil nil ("Issue3417.agda" . 222)) '(227 230 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 208)) '(232 241 (function) nil nil ("Issue3417.agda" . 167)) '(242 243 (bound) nil nil ("Issue3417.agda" . 222)) '(246 254 (function) nil nil ("Issue3417.agda" . 246)) '(257 260 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)) '(263 266 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)) '(267 275 (function) nil nil ("Issue3417.agda" . 246)) '(276 280 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 195)) '(283 287 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 195)) '(289 300 (function) nil nil ("Issue3417.agda" . 289)) '(303 306 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(307 318 (function) nil nil ("Issue3417.agda" . 289)) '(321 332 (function) nil nil ("Issue3417.agda" . 289)) '(339 349 (datatype) nil nil ("Issue3417.agda" . 339)) '(352 355 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(364 367 (inductiveconstructor) nil nil ("Issue3417.agda" . 364)) '(371 381 (datatype) nil nil ("Issue3417.agda" . 339)) '(384 387 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)) '(391 401 (datatype) nil nil ("Issue3417.agda" . 339)) '(403 411 (function) nil nil ("Issue3417.agda" . 403)) '(414 417 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(418 426 (function) nil nil ("Issue3417.agda" . 403)) '(429 432 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(137 141 (keyword) t) '(142 148 (keyword) t) '(149 165 (module) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 1)))
(agda2-highlight-add-annotations 'nil '(207 244 (deadcode)))
(agda2-highlight-add-annotations 'nil '(167 176 (function) nil nil ("Issue3417.agda" . 167)) '(179 182 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)) '(185 188 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)))
(agda2-highlight-add-annotations 'nil '(167 176 (function) nil nil ("Issue3417.agda" . 167)) '(189 198 (function) nil nil ("Issue3417.agda" . 167)) '(199 202 (bound) nil nil ("Issue3417.agda" . 199)) '(203 204 (symbol) t) '(205 206 (number) t) '(207 216 (function) nil nil ("Issue3417.agda" . 167)) '(217 218 (symbol) t) '(218 221 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 208)) '(222 223 (bound) nil nil ("Issue3417.agda" . 222)) '(223 224 (symbol) t) '(225 226 (symbol) t) '(227 230 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 208)) '(231 232 (symbol) t) '(232 241 (function) nil nil ("Issue3417.agda" . 167)) '(242 243 (bound) nil nil ("Issue3417.agda" . 222)) '(243 244 (symbol) t))
(agda2-highlight-add-annotations 'nil '(267 280 (coverageproblem)))
(agda2-highlight-add-annotations 'nil '(246 254 (function) nil nil ("Issue3417.agda" . 246)) '(257 260 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)) '(263 266 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)))
(agda2-highlight-add-annotations 'nil '(246 254 (function) nil nil ("Issue3417.agda" . 246)) '(267 275 (function) nil nil ("Issue3417.agda" . 246)) '(276 280 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 195)) '(281 282 (symbol) t) '(283 287 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 195)))
(agda2-highlight-add-annotations 'nil '(289 300 (function) nil nil ("Issue3417.agda" . 289)) '(303 306 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(289 300 (function) nil nil ("Issue3417.agda" . 289)) '(307 318 (function) nil nil ("Issue3417.agda" . 289)) '(319 320 (symbol) t) '(321 332 (function) nil nil ("Issue3417.agda" . 289)))
(agda2-highlight-add-annotations 'nil '(289 300 (terminationproblem)) '(321 332 (terminationproblem)))
(agda2-highlight-add-annotations 'nil '(339 349 (datatype) nil nil ("Issue3417.agda" . 339)) '(350 351 (symbol) t) '(352 355 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(334 338 (keyword) t) '(339 349 (datatype) nil nil ("Issue3417.agda" . 339)) '(356 361 (keyword) t) '(364 367 (inductiveconstructor) nil nil ("Issue3417.agda" . 364)) '(368 369 (symbol) t) '(370 371 (symbol) t) '(371 381 (datatype) nil nil ("Issue3417.agda" . 339)) '(382 383 (symbol) t) '(384 387 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Nat.agda" . 177)) '(387 388 (symbol) t) '(389 390 (symbol) t) '(391 401 (datatype) nil nil ("Issue3417.agda" . 339)))
(agda2-highlight-add-annotations 'nil '(339 349 (positivityproblem)) '(371 381 (positivityproblem)))
(agda2-info-action "*Error*" "———— Error ————————————————————————————————————————————————— Issue3417.agda:22,12-15 Set₁ != Set when checking that the expression Set has type Set ———— Warning(s) ———————————————————————————————————————————— Issue3417.agda:10,1-38 Unreachable clause when checking the definition of reachable Issue3417.agda:13,1-14 Incomplete pattern matching for coverage. Missing cases: coverage (suc x) when checking the definition of coverage Issue3417.agda:15,1-16,26 Termination checking failed for the following functions: Termination Problematic calls: Termination (at Issue3417.agda:16,15-26) Issue3417.agda:18,1-19,40 Positivity is not strictly positive, because it occurs to the left of an arrow in the type of the constructor abs in the definition of Positivity." nil)
((last . 3) . (agda2-maybe-goto '("Issue3417.agda" . 429)))
(agda2-highlight-add-annotations 'nil '(429 432 (error) nil "Issue3417.agda:22,12-15 Set₁ != Set when checking that the expression Set has type Set"))
(agda2-status-action "")
