(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(1 7 (keyword) t) '(28 33 (keyword) t) '(35 39 (keyword) t) '(42 43 (symbol) t) '(44 47 (primitivetype) t) '(48 53 (keyword) t) '(60 61 (symbol) t) '(62 63 (symbol) t) '(65 67 (symbol) t) '(69 70 (symbol) t) '(71 73 (symbol) t) '(77 81 (keyword) t) '(84 85 (symbol) t) '(86 89 (primitivetype) t) '(90 94 (keyword) t) '(97 98 (symbol) t) '(99 102 (primitivetype) t) '(104 108 (keyword) t) '(111 116 (keyword) t) '(123 124 (symbol) t) '(125 126 (symbol) t) '(128 130 (symbol) t) '(132 133 (symbol) t) '(134 136 (symbol) t) '(140 144 (keyword) t) '(147 152 (keyword) t) '(159 160 (symbol) t) '(163 165 (symbol) t) '(169 175 (keyword) t) '(178 179 (symbol) t) '(180 183 (primitivetype) t) '(184 189 (keyword) t) '(192 201 (keyword) t) '(204 209 (keyword) t) '(219 220 (symbol) t) '(223 225 (symbol) t) '(234 235 (symbol) t) '(236 239 (primitivetype) t) '(240 242 (symbol) t) '(243 246 (primitivetype) t) '(254 255 (symbol) t) '(258 260 (symbol) t) '(264 268 (keyword) t) '(271 272 (symbol) t) '(273 276 (primitivetype) t) '(277 282 (keyword) t) '(289 290 (symbol) t) '(298 300 (symbol) t) '(304 308 (keyword) t) '(311 312 (symbol) t) '(314 315 (symbol) t) '(316 319 (primitivetype) t) '(320 322 (symbol) t) '(323 326 (primitivetype) t) '(326 327 (symbol) t) '(328 329 (symbol) t) '(330 333 (primitivetype) t) '(334 339 (keyword) t) '(346 347 (symbol) t) '(350 351 (symbol) t) '(354 355 (symbol) t) '(356 358 (symbol) t) '(364 368 (keyword) t) '(369 375 (keyword) t) '(395 399 (keyword) t) '(403 404 (symbol) t) '(405 408 (primitivetype) t) '(412 413 (symbol) t) '(419 421 (symbol) t) '(422 425 (primitivetype) t) '(427 431 (keyword) t) '(435 440 (keyword) t) '(448 449 (symbol) t) '(450 451 (symbol) t) '(454 455 (symbol) t) '(461 463 (symbol) t) '(477 478 (symbol) t) '(492 493 (symbol) t) '(497 499 (symbol) t) '(506 510 (keyword) t) '(511 517 (keyword) t) '(541 545 (keyword) t) '(548 549 (symbol) t) '(550 553 (primitivetype) t) '(554 559 (keyword) t) '(566 567 (symbol) t) '(568 569 (symbol) t) '(572 573 (symbol) t) '(578 579 (symbol) t) '(579 580 (symbol) t) '(581 582 (symbol) t) '(584 585 (symbol) t) '(587 588 (symbol) t) '(589 590 (symbol) t) '(592 593 (symbol) t) '(594 596 (symbol) t) '(599 628 (comment) t) '(668 696 (comment) t))
(agda2-highlight-add-annotations 'nil '(1 7 (keyword) t) '(8 27 (module) nil nil ("HighlightPositivity.agda" . 1)) '(28 33 (keyword) t) '(40 41 (datatype) nil nil ("HighlightPositivity.agda" . 40)) '(56 59 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 56)) '(63 64 (datatype) nil nil ("HighlightPositivity.agda" . 40)) '(68 69 (datatype) nil nil ("HighlightPositivity.agda" . 40)) '(74 75 (datatype) nil nil ("HighlightPositivity.agda" . 40)) '(82 83 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(95 96 (datatype) nil nil ("HighlightPositivity.agda" . 95)) '(109 110 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(119 122 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 119)) '(126 127 (datatype) nil nil ("HighlightPositivity.agda" . 95)) '(131 132 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(137 138 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(145 146 (datatype) nil nil ("HighlightPositivity.agda" . 95)) '(155 158 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 155)) '(161 162 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(166 167 (datatype) nil nil ("HighlightPositivity.agda" . 95)) '(176 177 (record) nil nil ("HighlightPositivity.agda" . 176)) '(214 218 (field) nil nil ("HighlightPositivity.agda" . 214)) '(221 222 (record) nil nil ("HighlightPositivity.agda" . 176)) '(226 227 (record) nil nil ("HighlightPositivity.agda" . 176)) '(229 233 (function) nil nil ("HighlightPositivity.agda" . 229)) '(247 251 (function) nil nil ("HighlightPositivity.agda" . 229)) '(252 253 (bound) nil nil ("HighlightPositivity.agda" . 252)) '(256 257 (bound) nil nil ("HighlightPositivity.agda" . 252)) '(261 262 (bound) nil nil ("HighlightPositivity.agda" . 252)) '(269 270 (datatype) nil nil ("HighlightPositivity.agda" . 269)) '(285 288 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 285)) '(291 295 (function) nil nil ("HighlightPositivity.agda" . 229)) '(296 297 (datatype) nil nil ("HighlightPositivity.agda" . 269)) '(301 302 (datatype) nil nil ("HighlightPositivity.agda" . 269)) '(309 310 (datatype) nil nil ("HighlightPositivity.agda" . 309)) '(312 313 (bound) nil nil ("HighlightPositivity.agda" . 312)) '(342 345 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 342)) '(348 349 (bound) nil nil ("HighlightPositivity.agda" . 312)) '(351 352 (datatype) nil nil ("HighlightPositivity.agda" . 309)) '(353 354 (bound) nil nil ("HighlightPositivity.agda" . 312)) '(359 360 (datatype) nil nil ("HighlightPositivity.agda" . 309)) '(361 362 (bound) nil nil ("HighlightPositivity.agda" . 312)) '(376 393 (module) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 1)) '(400 402 (datatype) nil nil ("HighlightPositivity.agda" . 400)) '(409 411 (function) nil nil ("HighlightPositivity.agda" . 409)) '(414 418 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 67)) '(432 434 (datatype) nil nil ("HighlightPositivity.agda" . 400)) '(443 447 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 443)) '(452 453 (bound) nil nil ("HighlightPositivity.agda" . 452)) '(456 458 (function) nil nil ("HighlightPositivity.agda" . 409)) '(459 460 (bound) nil nil ("HighlightPositivity.agda" . 452)) '(464 466 (datatype) nil nil ("HighlightPositivity.agda" . 400)) '(468 470 (function) nil nil ("HighlightPositivity.agda" . 409)) '(471 476 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 86)) '(479 483 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 67)) '(484 486 (function) nil nil ("HighlightPositivity.agda" . 409)) '(487 491 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 92)) '(494 496 (datatype) nil nil ("HighlightPositivity.agda" . 400)) '(500 504 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 67)) '(518 539 (module) nil nil ("agda-default-include-path/Agda/Builtin/Equality.agda" . 1)) '(546 547 (datatype) nil nil ("HighlightPositivity.agda" . 546)) '(562 565 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 562)) '(570 571 (bound) nil nil ("HighlightPositivity.agda" . 570)) '(574 575 (bound) nil nil ("HighlightPositivity.agda" . 570)) '(576 577 (datatype operator) nil nil ("agda-default-include-path/Agda/Builtin/Equality.agda" . 83)) '(582 583 (bound) nil nil ("HighlightPositivity.agda" . 582)) '(586 587 (datatype) nil nil ("HighlightPositivity.agda" . 546)) '(591 592 (bound) nil nil ("HighlightPositivity.agda" . 582)) '(597 598 (datatype) nil nil ("HighlightPositivity.agda" . 546)))
(agda2-highlight-add-annotations 'nil '(40 41 (datatype) nil nil ("HighlightPositivity.agda" . 40)) '(42 43 (symbol) t) '(44 47 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(35 39 (keyword) t) '(40 41 (datatype) nil nil ("HighlightPositivity.agda" . 40)) '(48 53 (keyword) t) '(56 59 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 56)) '(60 61 (symbol) t) '(62 63 (symbol) t) '(63 64 (datatype) nil nil ("HighlightPositivity.agda" . 40)) '(65 67 (symbol) t) '(68 69 (datatype) nil nil ("HighlightPositivity.agda" . 40)) '(69 70 (symbol) t) '(71 73 (symbol) t) '(74 75 (datatype) nil nil ("HighlightPositivity.agda" . 40)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(82 83 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(84 85 (symbol) t) '(86 89 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(95 96 (datatype) nil nil ("HighlightPositivity.agda" . 95)) '(97 98 (symbol) t) '(99 102 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(104 108 (keyword) t) '(109 110 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(111 116 (keyword) t) '(119 122 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 119)) '(123 124 (symbol) t) '(125 126 (symbol) t) '(126 127 (datatype) nil nil ("HighlightPositivity.agda" . 95)) '(128 130 (symbol) t) '(131 132 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(132 133 (symbol) t) '(134 136 (symbol) t) '(137 138 (datatype) nil nil ("HighlightPositivity.agda" . 82)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(140 144 (keyword) t) '(145 146 (datatype) nil nil ("HighlightPositivity.agda" . 95)) '(147 152 (keyword) t) '(155 158 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 155)) '(159 160 (symbol) t) '(161 162 (datatype) nil nil ("HighlightPositivity.agda" . 82)) '(163 165 (symbol) t) '(166 167 (datatype) nil nil ("HighlightPositivity.agda" . 95)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (record) nil nil ("HighlightPositivity.agda" . 176)) '(178 179 (symbol) t) '(180 183 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(169 175 (keyword) t) '(176 177 (record) nil nil ("HighlightPositivity.agda" . 176)) '(184 189 (keyword) t) '(192 201 (keyword) t) '(204 209 (keyword) t) '(214 218 (field) nil nil ("HighlightPositivity.agda" . 214)) '(219 220 (symbol) t) '(221 222 (record) nil nil ("HighlightPositivity.agda" . 176)) '(223 225 (symbol) t) '(226 227 (record) nil nil ("HighlightPositivity.agda" . 176)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(229 233 (function) nil nil ("HighlightPositivity.agda" . 229)) '(234 235 (symbol) t) '(236 239 (primitivetype) t) '(240 242 (symbol) t) '(243 246 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(229 233 (function) nil nil ("HighlightPositivity.agda" . 229)) '(247 251 (function) nil nil ("HighlightPositivity.agda" . 229)) '(252 253 (bound) nil nil ("HighlightPositivity.agda" . 252)) '(254 255 (symbol) t) '(256 257 (bound) nil nil ("HighlightPositivity.agda" . 252)) '(258 260 (symbol) t) '(261 262 (bound) nil nil ("HighlightPositivity.agda" . 252)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (datatype) nil nil ("HighlightPositivity.agda" . 269)) '(271 272 (symbol) t) '(273 276 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(264 268 (keyword) t) '(269 270 (datatype) nil nil ("HighlightPositivity.agda" . 269)) '(277 282 (keyword) t) '(285 288 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 285)) '(289 290 (symbol) t) '(291 295 (function) nil nil ("HighlightPositivity.agda" . 229)) '(296 297 (datatype) nil nil ("HighlightPositivity.agda" . 269)) '(298 300 (symbol) t) '(301 302 (datatype) nil nil ("HighlightPositivity.agda" . 269)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (datatype) nil nil ("HighlightPositivity.agda" . 309)) '(311 312 (symbol) t) '(312 313 (bound) nil nil ("HighlightPositivity.agda" . 312)) '(314 315 (symbol) t) '(316 319 (primitivetype) t) '(320 322 (symbol) t) '(323 326 (primitivetype) t) '(326 327 (symbol) t) '(328 329 (symbol) t) '(330 333 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(304 308 (keyword) t) '(309 310 (datatype) nil nil ("HighlightPositivity.agda" . 309)) '(312 313 (bound) nil nil ("HighlightPositivity.agda" . 312)) '(334 339 (keyword) t) '(342 345 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 342)) '(346 347 (symbol) t) '(348 349 (bound) nil nil ("HighlightPositivity.agda" . 312)) '(350 351 (symbol) t) '(351 352 (datatype) nil nil ("HighlightPositivity.agda" . 309)) '(353 354 (bound) nil nil ("HighlightPositivity.agda" . 312)) '(354 355 (symbol) t) '(356 358 (symbol) t) '(359 360 (datatype) nil nil ("HighlightPositivity.agda" . 309)) '(361 362 (bound) nil nil ("HighlightPositivity.agda" . 312)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(364 368 (keyword) t) '(369 375 (keyword) t) '(376 393 (module) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 1)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(400 402 (datatype) nil nil ("HighlightPositivity.agda" . 400)) '(403 404 (symbol) t) '(405 408 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(409 411 (function) nil nil ("HighlightPositivity.agda" . 409)) '(412 413 (symbol) t) '(414 418 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 67)) '(419 421 (symbol) t) '(422 425 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(427 431 (keyword) t) '(432 434 (datatype) nil nil ("HighlightPositivity.agda" . 400)) '(435 440 (keyword) t) '(443 447 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 443)) '(448 449 (symbol) t) '(450 451 (symbol) t) '(452 453 (bound) nil nil ("HighlightPositivity.agda" . 452)) '(454 455 (symbol) t) '(456 458 (function) nil nil ("HighlightPositivity.agda" . 409)) '(459 460 (bound) nil nil ("HighlightPositivity.agda" . 452)) '(461 463 (symbol) t) '(464 466 (datatype) nil nil ("HighlightPositivity.agda" . 400)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(409 411 (function) nil nil ("HighlightPositivity.agda" . 409)) '(468 470 (function) nil nil ("HighlightPositivity.agda" . 409)) '(471 476 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 86)) '(477 478 (symbol) t) '(479 483 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 67)) '(484 486 (function) nil nil ("HighlightPositivity.agda" . 409)) '(487 491 (inductiveconstructor) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 92)) '(492 493 (symbol) t) '(494 496 (datatype) nil nil ("HighlightPositivity.agda" . 400)) '(497 499 (symbol) t) '(500 504 (datatype) nil nil ("agda-default-include-path/Agda/Builtin/Bool.agda" . 67)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(432 434 (positivityproblem)) '(456 458 (positivityproblem)) '(494 496 (positivityproblem)) '(506 510 (keyword) t) '(511 517 (keyword) t) '(518 539 (module) nil nil ("agda-default-include-path/Agda/Builtin/Equality.agda" . 1)))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(432 434 (positivityproblem)) '(456 458 (positivityproblem)) '(494 496 (positivityproblem)) '(546 547 (datatype) nil nil ("HighlightPositivity.agda" . 546)) '(548 549 (symbol) t) '(550 553 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(432 434 (positivityproblem)) '(456 458 (positivityproblem)) '(494 496 (positivityproblem)) '(541 545 (keyword) t) '(546 547 (datatype) nil nil ("HighlightPositivity.agda" . 546)) '(554 559 (keyword) t) '(562 565 (inductiveconstructor) nil nil ("HighlightPositivity.agda" . 562)) '(566 567 (symbol) t) '(568 569 (symbol) t) '(570 571 (bound) nil nil ("HighlightPositivity.agda" . 570)) '(572 573 (symbol) t) '(574 575 (bound) nil nil ("HighlightPositivity.agda" . 570)) '(576 577 (datatype operator) nil nil ("agda-default-include-path/Agda/Builtin/Equality.agda" . 83)) '(578 579 (symbol) t) '(579 580 (symbol) t) '(581 582 (symbol) t) '(582 583 (bound) nil nil ("HighlightPositivity.agda" . 582)) '(584 585 (symbol) t) '(586 587 (datatype) nil nil ("HighlightPositivity.agda" . 546)) '(587 588 (symbol) t) '(589 590 (symbol) t) '(591 592 (bound) nil nil ("HighlightPositivity.agda" . 582)) '(592 593 (symbol) t) '(594 596 (symbol) t) '(597 598 (datatype) nil nil ("HighlightPositivity.agda" . 546)))
(agda2-highlight-add-annotations 'nil '(1 7 (keyword) t) '(8 27 (module) nil nil ("HighlightPositivity.agda" . 1)) '(28 33 (keyword) t) '(40 41 (positivityproblem)) '(63 64 (positivityproblem)) '(109 110 (positivityproblem)) '(126 127 (positivityproblem)) '(145 146 (positivityproblem)) '(161 162 (positivityproblem)) '(176 177 (positivityproblem)) '(221 222 (positivityproblem)) '(269 270 (positivityproblem)) '(296 297 (positivityproblem)) '(309 310 (positivityproblem)) '(351 352 (positivityproblem)) '(432 434 (positivityproblem)) '(456 458 (positivityproblem)) '(494 496 (positivityproblem)) '(546 547 (positivityproblem)))
(agda2-highlight-add-annotations 'nil '(77 81 (keyword) t) '(90 94 (keyword) t) '(395 399 (keyword) t) '(599 628 (comment) t) '(668 696 (comment) t))
(agda2-status-action "")
(agda2-info-action "*All Errors*" "HighlightPositivity.agda:3,1-4,22 A is not strictly positive, because it occurs to the left of an arrow in the type of the constructor inA in the definition of A. HighlightPositivity.agda:6,6-13,15 B is not strictly positive, because it occurs in the type of the constructor inC in the definition of C, which occurs to the left of an arrow in the type of the constructor inB in the definition of B. HighlightPositivity.agda:6,6-13,15 C is not strictly positive, because it occurs to the left of an arrow in the type of the constructor inB in the definition of B, which occurs in the type of the constructor inC in the definition of C. HighlightPositivity.agda:15,1-18,18 D is not strictly positive, because it occurs to the left of an arrow in the definition of D. HighlightPositivity.agda:23,1-24,20 E is not strictly positive, because it occurs to the left of an arrow in the type of the constructor inE in the definition of E. HighlightPositivity.agda:26,1-27,23 F is not strictly positive, because it occurs in an argument to a bound variable in the type of the constructor inF in the definition of F. HighlightPositivity.agda:31,6-38,21 GU is not strictly positive, because it occurs to the left of an arrow in the second clause in the definition of GT, which occurs in the type of the constructor inGU in the definition of GU. HighlightPositivity.agda:42,1-43,39 H is not strictly positive, because it occurs to the left of an arrow in the type of the constructor inH in the definition of H. " nil)
((last . 1) . (agda2-goals-action '()))
