Agda2> (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear) (agda2-info-action "*Type-checking*" "Checking HighlightCopattern (HighlightCopattern.agda).\n" t) (agda2-highlight-add-annotations '(1 4 (symbol) nil) '(5 12 (keyword) nil) '(26 29 (symbol) nil) '(31 37 (keyword) nil) '(57 62 (keyword) nil) '(64 70 (keyword) nil) '(79 80 (symbol) nil) '(81 85 (primitivetype) nil) '(86 91 (keyword) nil) '(94 99 (keyword) nil) '(112 113 (symbol) nil) '(114 118 (primitivetype) nil) '(119 123 (keyword) nil) '(136 137 (symbol) nil) '(157 158 (symbol) nil) '(159 162 (primitivetype) nil) '(166 220 (comment) nil) '(227 228 (symbol) nil) '(237 238 (symbol) nil) '(239 243 (primitivetype) nil) '(251 252 (symbol) nil) '(264 318 (comment) nil)) (agda2-highlight-add-annotations '(31 37 (keyword) nil) '(38 56 (module) nil ("HighlightCopattern.agda" . 1)) '(57 62 (keyword) nil) '(71 78 (record) nil ("HighlightCopattern.agda" . 71)) '(104 111 (field) nil ("HighlightCopattern.agda" . 104)) '(124 131 (module) nil ("HighlightCopattern.agda" . 71)) '(133 135 (function) nil ("HighlightCopattern.agda" . 133)) '(138 145 (record) nil ("HighlightCopattern.agda" . 71)) '(146 153 (field) nil ("HighlightCopattern.agda" . 104)) '(154 156 (function) nil ("HighlightCopattern.agda" . 133)) '(222 226 (function) nil ("HighlightCopattern.agda" . 222)) '(229 236 (record) nil ("HighlightCopattern.agda" . 71)) '(244 248 (function) nil ("HighlightCopattern.agda" . 222)) '(249 250 (bound) nil ("HighlightCopattern.agda" . 249)) '(253 260 (field) nil ("HighlightCopattern.agda" . 104)) '(261 262 (bound) nil ("HighlightCopattern.agda" . 249))) (agda2-highlight-add-annotations '(71 78 (postulate) nil ("HighlightCopattern.agda" . 71)) '(79 80 (symbol) nil) '(81 85 (primitivetype) nil)) (agda2-highlight-add-annotations '(71 78 (record) nil ("HighlightCopattern.agda" . 71)) '(104 111 (field) nil ("HighlightCopattern.agda" . 104))) (agda2-highlight-add-annotations '(124 131 (module) nil ("HighlightCopattern.agda" . 71))) (agda2-highlight-add-annotations '(133 135 (function) nil ("HighlightCopattern.agda" . 133)) '(136 137 (symbol) nil) '(138 145 (record) nil ("HighlightCopattern.agda" . 71)) '(146 153 (field) nil ("HighlightCopattern.agda" . 104)) '(154 156 (function) nil ("HighlightCopattern.agda" . 133)) '(157 158 (symbol) nil) '(159 162 (primitivetype) nil)) (agda2-highlight-add-annotations '(222 226 (function) nil ("HighlightCopattern.agda" . 222)) '(227 228 (symbol) nil) '(229 236 (record) nil ("HighlightCopattern.agda" . 71)) '(237 238 (symbol) nil) '(239 243 (primitivetype) nil) '(244 248 (function) nil ("HighlightCopattern.agda" . 222)) '(249 250 (bound) nil ("HighlightCopattern.agda" . 249)) '(251 252 (symbol) nil) '(253 260 (field) nil ("HighlightCopattern.agda" . 104)) '(261 262 (bound) nil ("HighlightCopattern.agda" . 249))) (agda2-highlight-add-annotations '(31 37 (keyword) nil) '(38 56 (module) nil ("HighlightCopattern.agda" . 1)) '(57 62 (keyword) nil)) (agda2-highlight-add-annotations '(1 4 (symbol) nil) '(5 12 (keyword) nil) '(26 29 (symbol) nil) '(64 70 (keyword) nil) '(86 91 (keyword) nil) '(94 99 (keyword) nil) '(112 113 (symbol) nil) '(114 118 (primitivetype) nil) '(119 123 (keyword) nil) '(166 220 (comment) nil) '(264 318 (comment) nil)) (agda2-info-action "*Type-checking*" "Finished HighlightCopattern.\n" t) (agda2-status-action "Checked") (agda2-info-action "*All Goals*" "" nil) ((last . 1) . (agda2-goals-action '())) Agda2>