Agda2> (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear) (agda2-info-action "*Type-checking*" "Checking Issue758 (Issue758.agda).\n" t) (agda2-highlight-add-annotations '(2 6 (keyword) nil) '(11 12 (symbol) nil) '(13 16 (primitivetype) nil) '(17 22 (keyword) nil) '(30 31 (symbol) nil) '(43 44 (symbol) nil) '(49 50 (symbol) nil) '(56 63 (keyword) nil) '(75 76 (symbol) nil) '(81 82 (symbol) nil) '(87 88 (symbol) nil) '(92 93 (symbol) nil) '(98 99 (symbol) nil) '(106 107 (symbol) nil) '(117 118 (symbol) nil) '(119 120 (symbol) nil) '(127 128 (symbol) nil) '(136 137 (symbol) nil) '(138 139 (symbol) nil) '(161 162 (symbol) nil)) (agda2-highlight-add-annotations '(2 6 (keyword) nil) '(7 10 (datatype) nil ("Issue758.agda" . 7)) '(11 12 (symbol) nil) '(13 16 (primitivetype) nil) '(17 22 (keyword) nil) '(25 29 (inductiveconstructor) nil ("Issue758.agda" . 25)) '(30 31 (symbol) nil) '(32 35 (datatype) nil ("Issue758.agda" . 7)) '(38 41 (inductiveconstructor) nil ("Issue758.agda" . 38)) '(43 44 (symbol) nil) '(45 48 (datatype) nil ("Issue758.agda" . 7)) '(49 50 (symbol) nil) '(51 54 (datatype) nil ("Issue758.agda" . 7)) '(56 63 (keyword) nil) '(64 72 (inductiveconstructor) nil ("Issue758.agda" . 64)) '(73 74 (bound) nil ("Issue758.agda" . 86)) '(75 76 (symbol) nil) '(77 80 (inductiveconstructor) nil ("Issue758.agda" . 38)) '(81 82 (symbol) nil) '(82 85 (inductiveconstructor) nil ("Issue758.agda" . 38)) '(86 87 (bound) nil ("Issue758.agda" . 86)) '(87 88 (symbol) nil) '(90 91 (function) nil ("Issue758.agda" . 90)) '(92 93 (symbol) nil) '(94 97 (datatype) nil ("Issue758.agda" . 7)) '(98 99 (symbol) nil) '(100 103 (datatype) nil ("Issue758.agda" . 7)) '(104 105 (function) nil ("Issue758.agda" . 90)) '(106 107 (symbol) nil) '(107 115 (inductiveconstructor) nil ("Issue758.agda" . 64)) '(116 117 (bound) nil ("Issue758.agda" . 116)) '(117 118 (symbol) nil) '(119 120 (symbol) nil) '(121 122 (function) nil ("Issue758.agda" . 90)) '(123 124 (bound) nil ("Issue758.agda" . 116)) '(125 126 (function) nil ("Issue758.agda" . 90)) '(127 128 (symbol) nil) '(128 131 (inductiveconstructor) nil ("Issue758.agda" . 38)) '(132 136 (inductiveconstructor) nil ("Issue758.agda" . 25)) '(136 137 (symbol) nil) '(138 139 (symbol) nil) '(140 148 (inductiveconstructor) nil ("Issue758.agda" . 64)) '(149 153 (inductiveconstructor) nil ("Issue758.agda" . 25)) '(154 155 (function) nil ("Issue758.agda" . 90)) '(156 160 (inductiveconstructor) nil ("Issue758.agda" . 25)) '(161 162 (symbol) nil) '(163 167 (inductiveconstructor) nil ("Issue758.agda" . 25))) (agda2-highlight-add-annotations '(7 10 (datatype) nil ("Issue758.agda" . 7)) '(11 12 (symbol) nil) '(13 16 (primitivetype) nil) '(25 29 (inductiveconstructor) nil ("Issue758.agda" . 25)) '(32 35 (datatype) nil ("Issue758.agda" . 7)) '(38 41 (inductiveconstructor) nil ("Issue758.agda" . 38)) '(45 48 (datatype) nil ("Issue758.agda" . 7)) '(51 54 (datatype) nil ("Issue758.agda" . 7))) (agda2-highlight-add-annotations '(64 72 (inductiveconstructor) nil ("Issue758.agda" . 64)) '(73 74 (bound) nil ("Issue758.agda" . 86)) '(77 80 (inductiveconstructor) nil ("Issue758.agda" . 38)) '(82 85 (inductiveconstructor) nil ("Issue758.agda" . 38)) '(86 87 (bound) nil ("Issue758.agda" . 86))) (agda2-highlight-add-annotations '(90 91 (function) nil ("Issue758.agda" . 90)) '(92 93 (symbol) nil) '(94 97 (datatype) nil ("Issue758.agda" . 7)) '(98 99 (symbol) nil) '(100 103 (datatype) nil ("Issue758.agda" . 7)) '(104 105 (function) nil ("Issue758.agda" . 90)) '(106 107 (symbol) nil) '(107 115 (inductiveconstructor) nil ("Issue758.agda" . 64)) '(116 117 (bound) nil ("Issue758.agda" . 116)) '(117 118 (symbol) nil) '(119 120 (symbol) nil) '(121 122 (function) nil ("Issue758.agda" . 90)) '(123 124 (bound) nil ("Issue758.agda" . 116)) '(125 126 (function) nil ("Issue758.agda" . 90)) '(127 128 (symbol) nil) '(128 131 (inductiveconstructor) nil ("Issue758.agda" . 38)) '(132 136 (inductiveconstructor) nil ("Issue758.agda" . 25)) '(136 137 (symbol) nil) '(138 139 (symbol) nil) '(140 148 (inductiveconstructor) nil ("Issue758.agda" . 64)) '(149 153 (inductiveconstructor) nil ("Issue758.agda" . 25)) '(154 155 (function) nil ("Issue758.agda" . 90)) '(156 160 (inductiveconstructor) nil ("Issue758.agda" . 25)) '(161 162 (symbol) nil) '(163 167 (inductiveconstructor) nil ("Issue758.agda" . 25))) (agda2-highlight-add-annotations '(2 6 (keyword) nil) '(17 22 (keyword) nil) '(30 31 (symbol) nil) '(43 44 (symbol) nil) '(49 50 (symbol) nil) '(56 63 (keyword) nil) '(75 76 (symbol) nil) '(81 82 (symbol) nil) '(87 88 (symbol) nil)) (agda2-info-action "*Type-checking*" "Finished Issue758.\n" t) (agda2-status-action "Checked") (agda2-info-action "*All Goals*" "" nil) ((last . 1) . (agda2-goals-action '())) Agda2>