Agda2> (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear) (agda2-info-action "*Type-checking*" "Checking Highlighting (Highlighting.agda).\n" t) (agda2-info-action "*Type-checking*" " Checking Highlighting.M (Highlighting/M.agda).\n" t) (agda2-info-action "*Type-checking*" " Finished Highlighting.M.\n" t) (agda2-highlight-add-annotations '(1 7 (keyword) nil) '(21 26 (keyword) nil) '(36 37 (symbol) nil) '(38 42 (primitivetype) nil) '(51 52 (symbol) nil) '(53 57 (primitivetype) nil) '(59 65 (keyword) nil) '(68 69 (symbol) nil) '(71 72 (symbol) nil) '(73 76 (primitivetype) nil) '(76 77 (symbol) nil) '(78 79 (symbol) nil) '(88 93 (keyword) nil) '(96 107 (keyword) nil) '(115 120 (keyword) nil) '(123 124 (symbol) nil) '(125 128 (primitivetype) nil) '(134 135 (symbol) nil) '(136 139 (primitivetype) nil) '(140 141 (symbol) nil) '(142 145 (primitivetype) nil) '(146 147 (symbol) nil) '(148 151 (primitivetype) nil) '(160 161 (symbol) nil) '(167 172 (keyword) nil) '(175 176 (symbol) nil) '(183 184 (symbol) nil) '(185 188 (primitivetype) nil) '(194 195 (symbol) nil) '(202 203 (symbol) nil) '(204 207 (primitivetype) nil) '(212 213 (symbol) nil) '(217 226 (keyword) nil) '(229 230 (symbol) nil) '(231 232 (symbol) nil) '(234 238 (keyword) nil) '(239 245 (keyword) nil) '(262 266 (keyword) nil) '(269 270 (symbol) nil) '(272 273 (symbol) nil) '(274 277 (primitivetype) nil) '(277 278 (symbol) nil) '(279 280 (symbol) nil) '(289 294 (keyword) nil) '(299 300 (symbol) nil) '(301 304 (keyword) nil) '(307 308 (symbol) nil) '(311 313 (keyword) nil)) (agda2-highlight-add-annotations '(1 7 (keyword) nil) '(8 20 (module) nil ("Highlighting.agda" . 1)) '(21 26 (keyword) nil) '(28 35 (function) nil ("Highlighting.agda" . 28)) '(43 50 (function) nil ("Highlighting.agda" . 28)) '(66 67 (record) nil ("Highlighting.agda" . 66)) '(69 70 (bound) nil ("Highlighting.agda" . 69)) '(80 87 (function) nil ("Highlighting.agda" . 28)) '(108 111 (inductiveconstructor) nil ("Highlighting.agda" . 108)) '(121 122 (field) nil ("Highlighting.agda" . 121)) '(132 133 (bound) nil ("Highlighting.agda" . 132)) '(154 155 (function) nil ("Highlighting.agda" . 132)) '(156 157 (bound) nil ("Highlighting.agda" . 156)) '(158 159 (bound) nil ("Highlighting.agda" . 158)) '(162 163 (bound) nil ("Highlighting.agda" . 158)) '(173 174 (field) nil ("Highlighting.agda" . 173)) '(177 178 (bound) nil ("Highlighting.agda" . 132)) '(179 180 (bound) nil ("Highlighting.agda" . 69)) '(181 182 (bound) nil ("Highlighting.agda" . 121)) '(192 193 (function) nil ("Highlighting.agda" . 192)) '(196 197 (function) nil ("Highlighting.agda" . 132)) '(198 199 (bound) nil ("Highlighting.agda" . 69)) '(200 201 (field) nil ("Highlighting.agda" . 121)) '(210 211 (function) nil ("Highlighting.agda" . 192)) '(214 215 (function) nil ("Highlighting.agda" . 192)) '(227 228 (postulate) nil ("Highlighting.agda" . 227)) '(246 260 (module) nil ("Highlighting/M.agda" . 1)) '(267 268 (datatype) nil ("Highlighting.agda" . 267)) '(270 271 (bound) nil ("Highlighting.agda" . 270)) '(281 288 (function) nil ("Highlighting.agda" . 28)) '(297 298 (inductiveconstructor) nil ("Highlighting.agda" . 297)) '(305 306 (bound) nil ("Highlighting.agda" . 305)) '(309 310 (datatype) nil ("Highlighting.agda" . 267)) '(314 315 (bound) nil ("Highlighting.agda" . 305)) '(316 317 (bound) nil ("Highlighting.agda" . 270))) (agda2-highlight-add-annotations '(28 35 (function) nil ("Highlighting.agda" . 28)) '(36 37 (symbol) nil) '(38 42 (primitivetype) nil) '(43 50 (function) nil ("Highlighting.agda" . 28)) '(51 52 (symbol) nil) '(53 57 (primitivetype) nil)) (agda2-highlight-add-annotations '(66 67 (postulate) nil ("Highlighting.agda" . 66)) '(68 69 (symbol) nil) '(69 70 (bound) nil ("Highlighting.agda" . 69)) '(71 72 (symbol) nil) '(73 76 (primitivetype) nil) '(76 77 (symbol) nil) '(78 79 (symbol) nil) '(80 87 (function) nil ("Highlighting.agda" . 28))) (agda2-highlight-add-annotations '(132 133 (function) nil ("Highlighting.agda" . 132)) '(134 135 (symbol) nil) '(136 139 (primitivetype) nil) '(140 141 (symbol) nil) '(142 145 (primitivetype) nil) '(146 147 (symbol) nil) '(148 151 (primitivetype) nil) '(154 155 (function) nil ("Highlighting.agda" . 132)) '(156 157 (bound) nil ("Highlighting.agda" . 156)) '(158 159 (bound) nil ("Highlighting.agda" . 158)) '(160 161 (symbol) nil) '(162 163 (bound) nil ("Highlighting.agda" . 158))) (agda2-highlight-add-annotations '(192 193 (terminationproblem function) nil ("Highlighting.agda" . 192)) '(194 195 (symbol) nil) '(196 197 (function) nil ("Highlighting.agda" . 132)) '(198 199 (bound) nil ("Highlighting.agda" . 69)) '(200 201 (field) nil ("Highlighting.agda" . 121)) '(202 203 (symbol) nil) '(204 207 (primitivetype) nil) '(210 211 (function) nil ("Highlighting.agda" . 192)) '(212 213 (symbol) nil) '(214 215 (terminationproblem function) nil ("Highlighting.agda" . 192))) (agda2-highlight-add-annotations '(66 67 (record) nil ("Highlighting.agda" . 66)) '(108 111 (inductiveconstructor) nil ("Highlighting.agda" . 108)) '(121 122 (field) nil ("Highlighting.agda" . 121)) '(132 133 (bound) nil ("Highlighting.agda" . 132)) '(156 157 (bound) nil ("Highlighting.agda" . 156)) '(158 159 (bound) nil ("Highlighting.agda" . 158)) '(162 163 (bound) nil ("Highlighting.agda" . 158)) '(173 174 (field) nil ("Highlighting.agda" . 173)) '(177 178 (bound) nil ("Highlighting.agda" . 132)) '(179 180 (bound) nil ("Highlighting.agda" . 69)) '(181 182 (bound) nil ("Highlighting.agda" . 121))) (agda2-highlight-add-annotations '(227 228 (postulate) nil ("Highlighting.agda" . 227)) '(229 230 (symbol) nil) '(231 232 (symbol) nil)) (agda2-highlight-add-annotations '(246 260 (module) nil ("Highlighting/M.agda" . 1))) (agda2-highlight-add-annotations '(267 268 (datatype) nil ("Highlighting.agda" . 267)) '(269 270 (symbol) nil) '(270 271 (bound) nil ("Highlighting.agda" . 270)) '(272 273 (symbol) nil) '(274 277 (primitivetype) nil) '(277 278 (symbol) nil) '(279 280 (symbol) nil) '(281 288 (function) nil ("Highlighting.agda" . 28)) '(297 298 (inductiveconstructor) nil ("Highlighting.agda" . 297)) '(305 306 (bound) nil ("Highlighting.agda" . 305)) '(309 310 (datatype) nil ("Highlighting.agda" . 267)) '(314 315 (bound) nil ("Highlighting.agda" . 305)) '(316 317 (bound) nil ("Highlighting.agda" . 270))) (agda2-highlight-add-annotations '(1 7 (keyword) nil) '(8 20 (module) nil ("Highlighting.agda" . 1)) '(21 26 (keyword) nil)) (agda2-highlight-add-annotations '(59 65 (keyword) nil) '(88 93 (keyword) nil) '(96 107 (keyword) nil) '(115 120 (keyword) nil) '(123 124 (symbol) nil) '(125 128 (primitivetype) nil) '(167 172 (keyword) nil) '(175 176 (symbol) nil) '(183 184 (symbol) nil) '(185 188 (primitivetype) nil) '(217 226 (keyword) nil) '(234 238 (keyword) nil) '(239 245 (keyword) nil) '(262 266 (keyword) nil) '(289 294 (keyword) nil) '(299 300 (symbol) nil) '(301 304 (keyword) nil) '(307 308 (symbol) nil) '(311 313 (keyword) nil)) (agda2-highlight-add-annotations '(231 232 (unsolvedmeta) nil)) (agda2-info-action "*Type-checking*" "Finished Highlighting.\n" t) (agda2-status-action "") (agda2-info-action "*All Goals*" "Sort _4 [ at Highlighting.agda:19,15-16 ]\n_5 : Set _4 [ at Highlighting.agda:19,15-16 ]\n" nil) ((last . 1) . (agda2-goals-action '())) Agda2>