Agda2> (agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking With-flicker (With-flicker.agda).\n" t)
(agda2-highlight-add-annotations '(1 7 (keyword) nil) '(21 26 (keyword) nil) '(28 32 (keyword) nil) '(35 36 (symbol) nil) '(37 40 (primitivetype) nil) '(41 46 (keyword) nil) '(54 55 (symbol) nil) '(65 66 (symbol) nil) '(69 70 (symbol) nil) '(78 79 (symbol) nil) '(82 83 (symbol) nil) '(86 87 (symbol) nil) '(100 101 (symbol) nil) '(114 115 (symbol) nil) '(120 121 (symbol) nil) '(126 127 (symbol) nil) '(133 134 (symbol) nil) '(137 138 (symbol) nil) '(159 160 (symbol) nil) '(170 171 (symbol) nil) '(179 180 (symbol) nil) '(184 185 (symbol) nil) '(199 200 (symbol) nil) '(204 205 (symbol) nil) '(210 211 (symbol) nil) '(211 212 (symbol) nil) '(213 214 (symbol) nil) '(227 228 (symbol) nil) '(233 234 (symbol) nil) '(245 246 (symbol) nil) '(251 252 (symbol) nil) '(256 257 (symbol) nil) '(261 262 (symbol) nil) '(266 267 (symbol) nil) '(271 272 (symbol) nil) '(276 277 (symbol) nil) '(281 282 (symbol) nil) '(286 287 (symbol) nil) '(291 292 (symbol) nil) '(296 297 (symbol) nil) '(301 302 (symbol) nil) '(306 307 (symbol) nil) '(315 316 (symbol) nil) '(316 317 (symbol) nil) '(317 318 (symbol) nil) '(318 319 (symbol) nil) '(319 320 (symbol) nil) '(320 321 (symbol) nil) '(321 322 (symbol) nil) '(322 323 (symbol) nil) '(323 324 (symbol) nil) '(324 325 (symbol) nil) '(325 326 (symbol) nil) '(326 327 (symbol) nil) '(329 338 (keyword) nil) '(343 344 (symbol) nil) '(347 348 (symbol) nil) '(349 352 (primitivetype) nil) '(357 358 (symbol) nil) '(362 424 (comment) nil) '(425 461 (comment) nil) '(467 468 (symbol) nil) '(471 472 (symbol) nil) '(476 477 (symbol) nil) '(489 490 (symbol) nil) '(490 491 (symbol) nil) '(492 493 (symbol) nil) '(494 498 (primitivetype) nil) '(505 509 (keyword) nil) '(521 522 (symbol) nil) '(523 524 (symbol) nil) '(525 526 (symbol) nil) '(527 530 (primitivetype) nil))
(agda2-highlight-add-annotations '(1 7 (keyword) nil) '(8 20 (module) nil ("With-flicker.agda" . 1)) '(21 26 (keyword) nil) '(28 32 (keyword) nil) '(33 34 (datatype) nil ("With-flicker.agda" . 33)) '(35 36 (symbol) nil) '(37 40 (primitivetype) nil) '(41 46 (keyword) nil) '(49 53 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(54 55 (symbol) nil) '(56 57 (datatype) nil ("With-flicker.agda" . 33)) '(60 63 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(65 66 (symbol) nil) '(67 68 (datatype) nil ("With-flicker.agda" . 33)) '(69 70 (symbol) nil) '(71 72 (datatype) nil ("With-flicker.agda" . 33)) '(74 77 (function operator) nil ("With-flicker.agda" . 74)) '(78 79 (symbol) nil) '(80 81 (datatype) nil ("With-flicker.agda" . 33)) '(82 83 (symbol) nil) '(84 85 (datatype) nil ("With-flicker.agda" . 33)) '(86 87 (symbol) nil) '(88 89 (datatype) nil ("With-flicker.agda" . 33)) '(90 94 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(96 97 (function operator) nil ("With-flicker.agda" . 74)) '(98 99 (bound) nil ("With-flicker.agda" . 98)) '(100 101 (symbol) nil) '(102 103 (bound) nil ("With-flicker.agda" . 98)) '(104 107 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(108 109 (bound) nil ("With-flicker.agda" . 108)) '(110 111 (function operator) nil ("With-flicker.agda" . 74)) '(112 113 (bound) nil ("With-flicker.agda" . 112)) '(114 115 (symbol) nil) '(116 119 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(120 121 (symbol) nil) '(121 122 (bound) nil ("With-flicker.agda" . 108)) '(123 124 (function operator) nil ("With-flicker.agda" . 74)) '(125 126 (bound) nil ("With-flicker.agda" . 112)) '(126 127 (symbol) nil) '(129 132 (function) nil ("With-flicker.agda" . 129)) '(133 134 (symbol) nil) '(135 136 (datatype) nil ("With-flicker.agda" . 33)) '(137 138 (symbol) nil) '(139 140 (datatype) nil ("With-flicker.agda" . 33)) '(141 144 (function) nil ("With-flicker.agda" . 129)) '(145 149 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(159 160 (symbol) nil) '(161 165 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(166 169 (function) nil ("With-flicker.agda" . 129)) '(170 171 (symbol) nil) '(171 174 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(175 179 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(179 180 (symbol) nil) '(184 185 (symbol) nil) '(186 189 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(190 194 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(195 198 (function) nil ("With-flicker.agda" . 129)) '(199 200 (symbol) nil) '(200 203 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(204 205 (symbol) nil) '(205 208 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(209 210 (bound) nil ("With-flicker.agda" . 209)) '(210 211 (symbol) nil) '(211 212 (symbol) nil) '(213 214 (symbol) nil) '(215 218 (function) nil ("With-flicker.agda" . 129)) '(219 220 (bound) nil ("With-flicker.agda" . 209)) '(221 222 (function operator) nil ("With-flicker.agda" . 74)) '(223 226 (function) nil ("With-flicker.agda" . 129)) '(227 228 (symbol) nil) '(228 231 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(232 233 (bound) nil ("With-flicker.agda" . 209)) '(233 234 (symbol) nil) '(236 244 (function) nil ("With-flicker.agda" . 236)) '(245 246 (symbol) nil) '(247 250 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(251 252 (symbol) nil) '(252 255 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(256 257 (symbol) nil) '(257 260 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(261 262 (symbol) nil) '(262 265 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(266 267 (symbol) nil) '(267 270 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(271 272 (symbol) nil) '(272 275 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(276 277 (symbol) nil) '(277 280 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(281 282 (symbol) nil) '(282 285 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(286 287 (symbol) nil) '(287 290 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(291 292 (symbol) nil) '(292 295 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(296 297 (symbol) nil) '(297 300 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(301 302 (symbol) nil) '(302 305 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(306 307 (symbol) nil) '(307 310 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(311 315 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(315 316 (symbol) nil) '(316 317 (symbol) nil) '(317 318 (symbol) nil) '(318 319 (symbol) nil) '(319 320 (symbol) nil) '(320 321 (symbol) nil) '(321 322 (symbol) nil) '(322 323 (symbol) nil) '(323 324 (symbol) nil) '(324 325 (symbol) nil) '(325 326 (symbol) nil) '(326 327 (symbol) nil) '(329 338 (keyword) nil) '(341 342 (postulate) nil ("With-flicker.agda" . 341)) '(343 344 (symbol) nil) '(345 346 (datatype) nil ("With-flicker.agda" . 33)) '(347 348 (symbol) nil) '(349 352 (primitivetype) nil) '(355 356 (postulate) nil ("With-flicker.agda" . 355)) '(357 358 (symbol) nil) '(359 360 (datatype) nil ("With-flicker.agda" . 33)) '(362 424 (comment) nil) '(425 461 (comment) nil) '(463 466 (function) nil ("With-flicker.agda" . 463)) '(467 468 (symbol) nil) '(469 470 (postulate) nil ("With-flicker.agda" . 341)) '(471 472 (symbol) nil) '(472 475 (function) nil ("With-flicker.agda" . 129)) '(476 477 (symbol) nil) '(477 485 (function) nil ("With-flicker.agda" . 236)) '(486 487 (function operator) nil ("With-flicker.agda" . 74)) '(488 489 (postulate) nil ("With-flicker.agda" . 355)) '(489 490 (symbol) nil) '(490 491 (symbol) nil) '(492 493 (symbol) nil) '(494 498 (primitivetype) nil) '(499 502 (function) nil ("With-flicker.agda" . 463)) '(503 504 (bound) nil ("With-flicker.agda" . 503)) '(505 509 (keyword) nil) '(510 514 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(515 518 (function) nil ("With-flicker.agda" . 463)) '(519 520 (bound) nil ("With-flicker.agda" . 519)) '(521 522 (symbol) nil) '(523 524 (symbol) nil) '(525 526 (symbol) nil) '(527 530 (primitivetype) nil))
(agda2-highlight-add-annotations '(37 40 (typechecks) nil))
(agda2-highlight-add-annotations '(37 40 () nil))
(agda2-highlight-add-annotations '(37 40 (typechecks) nil))
(agda2-highlight-add-annotations '(37 40 () nil))
(agda2-highlight-add-annotations '(33 34 (typechecks) nil))
(agda2-highlight-add-annotations '(49 57 (typechecks) nil))
(agda2-highlight-add-annotations '(49 56 () nil))
(agda2-highlight-add-annotations '(49 56 (typechecks) nil))
(agda2-highlight-add-annotations '(49 57 () nil))
(agda2-highlight-add-annotations '(60 72 (typechecks) nil))
(agda2-highlight-add-annotations '(60 67 () nil))
(agda2-highlight-add-annotations '(68 72 () nil))
(agda2-highlight-add-annotations '(68 72 (typechecks) nil))
(agda2-highlight-add-annotations '(67 71 () nil))
(agda2-highlight-add-annotations '(67 71 (typechecks) nil))
(agda2-highlight-add-annotations '(60 67 (typechecks) nil))
(agda2-highlight-add-annotations '(60 72 () nil))
(agda2-highlight-add-annotations '(33 34 () nil))
(agda2-highlight-add-annotations '(33 34 (datatype) nil ("With-flicker.agda" . 33)) '(35 36 (symbol) nil) '(37 40 (primitivetype) nil) '(49 53 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(56 57 (datatype) nil ("With-flicker.agda" . 33)) '(60 63 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(67 68 (datatype) nil ("With-flicker.agda" . 33)) '(71 72 (datatype) nil ("With-flicker.agda" . 33)))
(agda2-highlight-add-annotations '(80 89 (typechecks) nil))
(agda2-highlight-add-annotations '(81 89 () nil))
(agda2-highlight-add-annotations '(81 89 (typechecks) nil))
(agda2-highlight-add-annotations '(80 84 () nil))
(agda2-highlight-add-annotations '(85 89 () nil))
(agda2-highlight-add-annotations '(85 89 (typechecks) nil))
(agda2-highlight-add-annotations '(84 88 () nil))
(agda2-highlight-add-annotations '(84 88 (typechecks) nil))
(agda2-highlight-add-annotations '(80 84 (typechecks) nil))
(agda2-highlight-add-annotations '(80 89 () nil))
(agda2-highlight-add-annotations '(80 89 (typechecks) nil))
(agda2-highlight-add-annotations '(80 89 () nil))
(agda2-highlight-add-annotations '(90 103 (typechecks) nil) '(104 127 (typechecks) nil))
(agda2-highlight-add-annotations '(90 103 () nil) '(104 127 () nil))
(agda2-highlight-add-annotations '(90 103 (typechecks) nil))
(agda2-highlight-add-annotations '(94 103 () nil))
(agda2-highlight-add-annotations '(94 103 (typechecks) nil))
(agda2-highlight-add-annotations '(94 103 () nil))
(agda2-highlight-add-annotations '(94 103 (typechecks) nil))
(agda2-highlight-add-annotations '(90 102 () nil))
(agda2-highlight-add-annotations '(90 102 (typechecks) nil))
(agda2-highlight-add-annotations '(90 103 () nil))
(agda2-highlight-add-annotations '(104 127 (typechecks) nil))
(agda2-highlight-add-annotations '(109 127 () nil))
(agda2-highlight-add-annotations '(109 127 (typechecks) nil))
(agda2-highlight-add-annotations '(109 127 () nil))
(agda2-highlight-add-annotations '(109 127 (typechecks) nil))
(agda2-highlight-add-annotations '(104 116 () nil))
(agda2-highlight-add-annotations '(119 127 () nil))
(agda2-highlight-add-annotations '(121 126 (typechecks) nil))
(agda2-highlight-add-annotations '(121 123 () nil) '(124 126 () nil))
(agda2-highlight-add-annotations '(121 123 (typechecks) nil) '(124 126 (typechecks) nil))
(agda2-highlight-add-annotations '(121 123 () nil) '(124 126 () nil))
(agda2-highlight-add-annotations '(121 122 (typechecks) nil))
(agda2-highlight-add-annotations '(121 122 () nil))
(agda2-highlight-add-annotations '(125 126 (typechecks) nil))
(agda2-highlight-add-annotations '(125 126 () nil))
(agda2-highlight-add-annotations '(121 123 (typechecks) nil) '(124 126 (typechecks) nil))
(agda2-highlight-add-annotations '(121 126 () nil))
(agda2-highlight-add-annotations '(119 127 (typechecks) nil))
(agda2-highlight-add-annotations '(104 116 (typechecks) nil))
(agda2-highlight-add-annotations '(104 127 () nil))
(agda2-highlight-add-annotations '(90 103 (typechecks) nil) '(104 127 (typechecks) nil))
(agda2-highlight-add-annotations '(90 103 () nil) '(104 127 () nil))
(agda2-highlight-add-annotations '(74 77 (function operator) nil ("With-flicker.agda" . 74)) '(78 79 (symbol) nil) '(80 81 (datatype) nil ("With-flicker.agda" . 33)) '(82 83 (symbol) nil) '(84 85 (datatype) nil ("With-flicker.agda" . 33)) '(86 87 (symbol) nil) '(88 89 (datatype) nil ("With-flicker.agda" . 33)) '(90 94 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(96 97 (function operator) nil ("With-flicker.agda" . 74)) '(98 99 (bound) nil ("With-flicker.agda" . 98)) '(100 101 (symbol) nil) '(102 103 (bound) nil ("With-flicker.agda" . 98)) '(104 107 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(108 109 (bound) nil ("With-flicker.agda" . 108)) '(110 111 (function operator) nil ("With-flicker.agda" . 74)) '(112 113 (bound) nil ("With-flicker.agda" . 112)) '(114 115 (symbol) nil) '(116 119 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(120 121 (symbol) nil) '(121 122 (bound) nil ("With-flicker.agda" . 108)) '(123 124 (function operator) nil ("With-flicker.agda" . 74)) '(125 126 (bound) nil ("With-flicker.agda" . 112)) '(126 127 (symbol) nil))
(agda2-highlight-add-annotations '(135 140 (typechecks) nil))
(agda2-highlight-add-annotations '(136 140 () nil))
(agda2-highlight-add-annotations '(136 140 (typechecks) nil))
(agda2-highlight-add-annotations '(135 139 () nil))
(agda2-highlight-add-annotations '(135 139 (typechecks) nil))
(agda2-highlight-add-annotations '(135 140 () nil))
(agda2-highlight-add-annotations '(135 140 (typechecks) nil))
(agda2-highlight-add-annotations '(135 140 () nil))
(agda2-highlight-add-annotations '(141 165 (typechecks) nil) '(166 194 (typechecks) nil) '(195 234 (typechecks) nil))
(agda2-highlight-add-annotations '(141 165 () nil) '(166 194 () nil) '(195 234 () nil))
(agda2-highlight-add-annotations '(141 165 (typechecks) nil))
(agda2-highlight-add-annotations '(141 145 () nil) '(149 165 () nil))
(agda2-highlight-add-annotations '(141 145 (typechecks) nil) '(149 165 (typechecks) nil))
(agda2-highlight-add-annotations '(141 145 () nil) '(149 165 () nil))
(agda2-highlight-add-annotations '(141 145 (typechecks) nil) '(149 165 (typechecks) nil))
(agda2-highlight-add-annotations '(141 161 () nil))
(agda2-highlight-add-annotations '(141 161 (typechecks) nil))
(agda2-highlight-add-annotations '(141 165 () nil))
(agda2-highlight-add-annotations '(166 194 (typechecks) nil))
(agda2-highlight-add-annotations '(166 171 () nil) '(179 194 () nil))
(agda2-highlight-add-annotations '(166 171 (typechecks) nil) '(179 194 (typechecks) nil))
(agda2-highlight-add-annotations '(166 171 () nil) '(179 194 () nil))
(agda2-highlight-add-annotations '(171 175 () nil))
(agda2-highlight-add-annotations '(171 175 (typechecks) nil))
(agda2-highlight-add-annotations '(171 175 () nil))
(agda2-highlight-add-annotations '(171 175 (typechecks) nil))
(agda2-highlight-add-annotations '(166 171 (typechecks) nil) '(179 194 (typechecks) nil))
(agda2-highlight-add-annotations '(166 186 () nil))
(agda2-highlight-add-annotations '(189 194 () nil))
(agda2-highlight-add-annotations '(190 194 (typechecks) nil))
(agda2-highlight-add-annotations '(190 194 () nil))
(agda2-highlight-add-annotations '(189 194 (typechecks) nil))
(agda2-highlight-add-annotations '(166 186 (typechecks) nil))
(agda2-highlight-add-annotations '(166 194 () nil))
(agda2-highlight-add-annotations '(195 234 (typechecks) nil))
(agda2-highlight-add-annotations '(195 200 () nil) '(210 234 () nil))
(agda2-highlight-add-annotations '(195 200 (typechecks) nil) '(210 234 (typechecks) nil))
(agda2-highlight-add-annotations '(195 200 () nil) '(210 234 () nil))
(agda2-highlight-add-annotations '(200 205 () nil))
(agda2-highlight-add-annotations '(200 205 (typechecks) nil))
(agda2-highlight-add-annotations '(200 205 () nil))
(agda2-highlight-add-annotations '(200 205 (typechecks) nil))
(agda2-highlight-add-annotations '(195 200 (typechecks) nil) '(210 234 (typechecks) nil))
(agda2-highlight-add-annotations '(195 215 () nil))
(agda2-highlight-add-annotations '(215 221 () nil) '(222 234 () nil))
(agda2-highlight-add-annotations '(215 221 (typechecks) nil) '(222 234 (typechecks) nil))
(agda2-highlight-add-annotations '(215 221 () nil) '(222 234 () nil))
(agda2-highlight-add-annotations '(215 220 (typechecks) nil))
(agda2-highlight-add-annotations '(218 220 () nil))
(agda2-highlight-add-annotations '(218 220 (typechecks) nil))
(agda2-highlight-add-annotations '(218 220 () nil))
(agda2-highlight-add-annotations '(219 220 (typechecks) nil))
(agda2-highlight-add-annotations '(219 220 () nil))
(agda2-highlight-add-annotations '(218 220 (typechecks) nil))
(agda2-highlight-add-annotations '(215 220 () nil))
(agda2-highlight-add-annotations '(223 234 (typechecks) nil))
(agda2-highlight-add-annotations '(226 234 () nil))
(agda2-highlight-add-annotations '(226 234 (typechecks) nil))
(agda2-highlight-add-annotations '(226 234 () nil))
(agda2-highlight-add-annotations '(228 233 (typechecks) nil))
(agda2-highlight-add-annotations '(231 233 () nil))
(agda2-highlight-add-annotations '(232 233 (typechecks) nil))
(agda2-highlight-add-annotations '(232 233 () nil))
(agda2-highlight-add-annotations '(231 233 (typechecks) nil))
(agda2-highlight-add-annotations '(228 233 () nil))
(agda2-highlight-add-annotations '(226 234 (typechecks) nil))
(agda2-highlight-add-annotations '(223 234 () nil))
(agda2-highlight-add-annotations '(215 221 (typechecks) nil) '(222 234 (typechecks) nil))
(agda2-highlight-add-annotations '(195 215 (typechecks) nil))
(agda2-highlight-add-annotations '(195 234 () nil))
(agda2-highlight-add-annotations '(141 165 (typechecks) nil) '(166 194 (typechecks) nil) '(195 234 (typechecks) nil))
(agda2-highlight-add-annotations '(141 165 () nil) '(166 194 () nil) '(195 234 () nil))
(agda2-highlight-add-annotations '(129 132 (function) nil ("With-flicker.agda" . 129)) '(133 134 (symbol) nil) '(135 136 (datatype) nil ("With-flicker.agda" . 33)) '(137 138 (symbol) nil) '(139 140 (datatype) nil ("With-flicker.agda" . 33)) '(141 144 (function) nil ("With-flicker.agda" . 129)) '(145 149 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(159 160 (symbol) nil) '(161 165 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(166 169 (function) nil ("With-flicker.agda" . 129)) '(170 171 (symbol) nil) '(171 174 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(175 179 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(179 180 (symbol) nil) '(184 185 (symbol) nil) '(186 189 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(190 194 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(195 198 (function) nil ("With-flicker.agda" . 129)) '(199 200 (symbol) nil) '(200 203 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(204 205 (symbol) nil) '(205 208 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(209 210 (bound) nil ("With-flicker.agda" . 209)) '(210 211 (symbol) nil) '(211 212 (symbol) nil) '(213 214 (symbol) nil) '(215 218 (function) nil ("With-flicker.agda" . 129)) '(219 220 (bound) nil ("With-flicker.agda" . 209)) '(221 222 (function operator) nil ("With-flicker.agda" . 74)) '(223 226 (function) nil ("With-flicker.agda" . 129)) '(227 228 (symbol) nil) '(228 231 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(232 233 (bound) nil ("With-flicker.agda" . 209)) '(233 234 (symbol) nil))
(agda2-highlight-add-annotations '(236 244 (typechecks) nil))
(agda2-highlight-add-annotations '(236 244 () nil))
(agda2-highlight-add-annotations '(236 244 (typechecks) nil))
(agda2-highlight-add-annotations '(236 244 () nil))
(agda2-highlight-add-annotations '(236 327 (typechecks) nil))
(agda2-highlight-add-annotations '(236 247 () nil))
(agda2-highlight-add-annotations '(250 327 () nil))
(agda2-highlight-add-annotations '(250 327 (typechecks) nil))
(agda2-highlight-add-annotations '(250 327 () nil))
(agda2-highlight-add-annotations '(252 326 (typechecks) nil))
(agda2-highlight-add-annotations '(255 326 () nil))
(agda2-highlight-add-annotations '(257 325 (typechecks) nil))
(agda2-highlight-add-annotations '(260 325 () nil))
(agda2-highlight-add-annotations '(262 324 (typechecks) nil))
(agda2-highlight-add-annotations '(265 324 () nil))
(agda2-highlight-add-annotations '(267 323 (typechecks) nil))
(agda2-highlight-add-annotations '(270 323 () nil))
(agda2-highlight-add-annotations '(272 322 (typechecks) nil))
(agda2-highlight-add-annotations '(275 322 () nil))
(agda2-highlight-add-annotations '(277 321 (typechecks) nil))
(agda2-highlight-add-annotations '(280 321 () nil))
(agda2-highlight-add-annotations '(282 320 (typechecks) nil))
(agda2-highlight-add-annotations '(285 320 () nil))
(agda2-highlight-add-annotations '(287 319 (typechecks) nil))
(agda2-highlight-add-annotations '(290 319 () nil))
(agda2-highlight-add-annotations '(292 318 (typechecks) nil))
(agda2-highlight-add-annotations '(295 318 () nil))
(agda2-highlight-add-annotations '(297 317 (typechecks) nil))
(agda2-highlight-add-annotations '(300 317 () nil))
(agda2-highlight-add-annotations '(302 316 (typechecks) nil))
(agda2-highlight-add-annotations '(305 316 () nil))
(agda2-highlight-add-annotations '(307 315 (typechecks) nil))
(agda2-highlight-add-annotations '(310 315 () nil))
(agda2-highlight-add-annotations '(311 315 (typechecks) nil))
(agda2-highlight-add-annotations '(311 315 () nil))
(agda2-highlight-add-annotations '(310 315 (typechecks) nil))
(agda2-highlight-add-annotations '(307 315 () nil))
(agda2-highlight-add-annotations '(305 316 (typechecks) nil))
(agda2-highlight-add-annotations '(302 316 () nil))
(agda2-highlight-add-annotations '(300 317 (typechecks) nil))
(agda2-highlight-add-annotations '(297 317 () nil))
(agda2-highlight-add-annotations '(295 318 (typechecks) nil))
(agda2-highlight-add-annotations '(292 318 () nil))
(agda2-highlight-add-annotations '(290 319 (typechecks) nil))
(agda2-highlight-add-annotations '(287 319 () nil))
(agda2-highlight-add-annotations '(285 320 (typechecks) nil))
(agda2-highlight-add-annotations '(282 320 () nil))
(agda2-highlight-add-annotations '(280 321 (typechecks) nil))
(agda2-highlight-add-annotations '(277 321 () nil))
(agda2-highlight-add-annotations '(275 322 (typechecks) nil))
(agda2-highlight-add-annotations '(272 322 () nil))
(agda2-highlight-add-annotations '(270 323 (typechecks) nil))
(agda2-highlight-add-annotations '(267 323 () nil))
(agda2-highlight-add-annotations '(265 324 (typechecks) nil))
(agda2-highlight-add-annotations '(262 324 () nil))
(agda2-highlight-add-annotations '(260 325 (typechecks) nil))
(agda2-highlight-add-annotations '(257 325 () nil))
(agda2-highlight-add-annotations '(255 326 (typechecks) nil))
(agda2-highlight-add-annotations '(252 326 () nil))
(agda2-highlight-add-annotations '(250 327 (typechecks) nil))
(agda2-highlight-add-annotations '(236 247 (typechecks) nil))
(agda2-highlight-add-annotations '(236 327 () nil))
(agda2-highlight-add-annotations '(236 244 (function) nil ("With-flicker.agda" . 236)) '(245 246 (symbol) nil) '(247 250 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(251 252 (symbol) nil) '(252 255 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(256 257 (symbol) nil) '(257 260 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(261 262 (symbol) nil) '(262 265 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(266 267 (symbol) nil) '(267 270 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(271 272 (symbol) nil) '(272 275 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(276 277 (symbol) nil) '(277 280 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(281 282 (symbol) nil) '(282 285 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(286 287 (symbol) nil) '(287 290 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(291 292 (symbol) nil) '(292 295 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(296 297 (symbol) nil) '(297 300 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(301 302 (symbol) nil) '(302 305 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(306 307 (symbol) nil) '(307 310 (inductiveconstructor) nil ("With-flicker.agda" . 60)) '(311 315 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(315 316 (symbol) nil) '(316 317 (symbol) nil) '(317 318 (symbol) nil) '(318 319 (symbol) nil) '(319 320 (symbol) nil) '(320 321 (symbol) nil) '(321 322 (symbol) nil) '(322 323 (symbol) nil) '(323 324 (symbol) nil) '(324 325 (symbol) nil) '(325 326 (symbol) nil) '(326 327 (symbol) nil))
(agda2-highlight-add-annotations '(345 352 (typechecks) nil))
(agda2-highlight-add-annotations '(346 352 () nil))
(agda2-highlight-add-annotations '(346 352 (typechecks) nil))
(agda2-highlight-add-annotations '(345 349 () nil))
(agda2-highlight-add-annotations '(345 349 (typechecks) nil))
(agda2-highlight-add-annotations '(345 352 () nil))
(agda2-highlight-add-annotations '(345 352 (typechecks) nil))
(agda2-highlight-add-annotations '(345 352 () nil))
(agda2-highlight-add-annotations '(341 342 (postulate) nil ("With-flicker.agda" . 341)) '(343 344 (symbol) nil) '(345 346 (datatype) nil ("With-flicker.agda" . 33)) '(347 348 (symbol) nil) '(349 352 (primitivetype) nil))
(agda2-highlight-add-annotations '(359 360 (typechecks) nil))
(agda2-highlight-add-annotations '(359 360 () nil))
(agda2-highlight-add-annotations '(359 360 (typechecks) nil))
(agda2-highlight-add-annotations '(359 360 () nil))
(agda2-highlight-add-annotations '(355 356 (postulate) nil ("With-flicker.agda" . 355)) '(357 358 (symbol) nil) '(359 360 (datatype) nil ("With-flicker.agda" . 33)))
(agda2-highlight-add-annotations '(469 498 (typechecks) nil))
(agda2-highlight-add-annotations '(491 498 () nil))
(agda2-highlight-add-annotations '(470 491 () nil))
(agda2-highlight-add-annotations '(470 491 (typechecks) nil))
(agda2-highlight-add-annotations '(470 491 () nil))
(agda2-highlight-add-annotations '(472 490 (typechecks) nil))
(agda2-highlight-add-annotations '(475 490 () nil))
(agda2-highlight-add-annotations '(475 490 (typechecks) nil))
(agda2-highlight-add-annotations '(475 490 () nil))
(agda2-highlight-add-annotations '(477 489 (typechecks) nil))
(agda2-highlight-add-annotations '(477 486 () nil) '(487 489 () nil))
(agda2-highlight-add-annotations '(477 486 (typechecks) nil) '(487 489 (typechecks) nil))
(agda2-highlight-add-annotations '(477 486 () nil) '(487 489 () nil))
(agda2-highlight-add-annotations '(477 485 (typechecks) nil))
(agda2-highlight-add-annotations '(477 485 () nil))
(agda2-highlight-add-annotations '(488 489 (typechecks) nil))
(agda2-highlight-add-annotations '(488 489 () nil))
(agda2-highlight-add-annotations '(477 486 (typechecks) nil) '(487 489 (typechecks) nil))
(agda2-highlight-add-annotations '(477 489 () nil))
(agda2-highlight-add-annotations '(475 490 (typechecks) nil))
(agda2-highlight-add-annotations '(472 490 () nil))
(agda2-highlight-add-annotations '(470 491 (typechecks) nil))
(agda2-highlight-add-annotations '(491 498 (typechecks) nil))
(agda2-highlight-add-annotations '(469 494 () nil))
(agda2-highlight-add-annotations '(469 494 (typechecks) nil))
(agda2-highlight-add-annotations '(469 498 () nil))
(agda2-highlight-add-annotations '(469 498 (typechecks) nil))
(agda2-highlight-add-annotations '(469 498 () nil))
(agda2-highlight-add-annotations '(499 514 (typechecks) nil) '(515 530 (typechecks) nil))
(agda2-highlight-add-annotations '(499 514 () nil) '(515 530 () nil))
(agda2-highlight-add-annotations '(499 514 (typechecks) nil) '(515 530 (typechecks) nil))
(agda2-highlight-add-annotations '(499 510 () nil) '(515 530 () nil))
(agda2-highlight-add-annotations '(499 510 (typechecks) nil) '(515 530 (typechecks) nil))
(agda2-highlight-add-annotations '(515 530 () nil))
(agda2-highlight-add-annotations '(515 530 (typechecks) nil))
(agda2-highlight-add-annotations '(499 514 () nil))
(agda2-highlight-add-annotations '(515 530 () nil))
(agda2-highlight-add-annotations '(515 530 (typechecks) nil))
(agda2-highlight-add-annotations '(515 527 () nil))
(agda2-highlight-add-annotations '(515 527 (typechecks) nil))
(agda2-highlight-add-annotations '(515 530 () nil))
(agda2-highlight-add-annotations '(515 530 (typechecks) nil))
(agda2-highlight-add-annotations '(499 514 (typechecks) nil))
(agda2-highlight-add-annotations '(499 514 () nil) '(515 530 () nil))
(agda2-highlight-add-annotations '(499 514 (typechecks) nil) '(515 530 (typechecks) nil))
(agda2-highlight-add-annotations '(499 514 () nil) '(515 530 () nil))
(agda2-highlight-add-annotations '(463 466 (function) nil ("With-flicker.agda" . 463)) '(467 468 (symbol) nil) '(469 470 (postulate) nil ("With-flicker.agda" . 341)) '(471 472 (symbol) nil) '(472 475 (function) nil ("With-flicker.agda" . 129)) '(476 477 (symbol) nil) '(477 485 (function) nil ("With-flicker.agda" . 236)) '(486 487 (function operator) nil ("With-flicker.agda" . 74)) '(488 489 (postulate) nil ("With-flicker.agda" . 355)) '(489 490 (symbol) nil) '(490 491 (symbol) nil) '(492 493 (symbol) nil) '(494 498 (primitivetype) nil) '(499 502 (function) nil ("With-flicker.agda" . 463)) '(503 504 (bound) nil ("With-flicker.agda" . 503)) '(505 509 (keyword) nil) '(510 514 (inductiveconstructor) nil ("With-flicker.agda" . 49)) '(515 518 (function) nil ("With-flicker.agda" . 463)) '(519 520 (bound) nil ("With-flicker.agda" . 519)) '(521 522 (symbol) nil) '(523 524 (symbol) nil) '(525 526 (symbol) nil) '(527 530 (primitivetype) nil))
(agda2-highlight-add-annotations '(1 7 (keyword) nil) '(8 20 (module) nil ("With-flicker.agda" . 1)) '(21 26 (keyword) nil) '(28 32 (keyword) nil) '(41 46 (keyword) nil) '(54 55 (symbol) nil) '(65 66 (symbol) nil) '(69 70 (symbol) nil) '(329 338 (keyword) nil) '(362 424 (comment) nil) '(425 461 (comment) nil))
(agda2-info-action "*Type-checking*" "Finished With-flicker.\n" t)
(agda2-status-action "Checked")
(agda2-info-action "*All Goals*" "" nil)
((last . 1) . (agda2-goals-action '()))
Agda2>