(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(1 5 (keyword) t) '(8 9 (symbol) t) '(10 13 (primitivetype) t) '(14 19 (keyword) t) '(21 27 (keyword) t) '(30 31 (symbol) t) '(32 35 (primitivetype) t) '(36 41 (keyword) t) '(44 55 (keyword) t) '(60 65 (keyword) t) '(68 69 (symbol) t) '(73 79 (keyword) t) '(83 84 (symbol) t) '(85 88 (primitivetype) t) '(89 94 (keyword) t) '(97 108 (keyword) t) '(111 122 (keyword) t) '(127 132 (keyword) t) '(135 136 (symbol) t) '(143 144 (symbol) t) '(147 148 (symbol) t) '(155 156 (symbol) t) '(157 160 (keyword) t) '(165 166 (symbol) t) '(169 171 (keyword) t))
(agda2-highlight-add-annotations 'nil '(6 7 (datatype) nil nil ("Issue1064.agda" . 6)) '(28 29 (record) nil nil ("Issue1064.agda" . 28)) '(56 57 (inductiveconstructor) nil nil ("Issue1064.agda" . 56)) '(66 67 (field) nil nil ("Issue1064.agda" . 66)) '(70 71 (datatype) nil nil ("Issue1064.agda" . 6)) '(80 82 (record) nil nil ("Issue1064.agda" . 80)) '(123 124 (inductiveconstructor) nil nil ("Issue1064.agda" . 123)) '(133 134 (field) nil nil ("Issue1064.agda" . 133)) '(137 139 (record) nil nil ("Issue1064.agda" . 80)) '(141 142 (function) nil nil ("Issue1064.agda" . 141)) '(145 146 (record) nil nil ("Issue1064.agda" . 28)) '(149 150 (datatype) nil nil ("Issue1064.agda" . 6)) '(151 152 (function) nil nil ("Issue1064.agda" . 141)) '(153 154 (bound) nil nil ("Issue1064.agda" . 153)) '(161 162 (inductiveconstructor)) '(163 164 (bound) nil nil ("Issue1064.agda" . 163)) '(167 168 (bound) nil nil ("Issue1064.agda" . 153)) '(172 173 (bound) nil nil ("Issue1064.agda" . 163)))
(agda2-highlight-add-annotations 'nil '(6 7 (datatype) nil nil ("Issue1064.agda" . 6)) '(8 9 (symbol) t) '(10 13 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(1 5 (keyword) t) '(6 7 (datatype) nil nil ("Issue1064.agda" . 6)) '(14 19 (keyword) t))
(agda2-highlight-add-annotations 'nil '(28 29 (record) nil nil ("Issue1064.agda" . 28)) '(30 31 (symbol) t) '(32 35 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(21 27 (keyword) t) '(28 29 (record) nil nil ("Issue1064.agda" . 28)) '(36 41 (keyword) t) '(44 55 (keyword) t) '(56 57 (inductiveconstructor) nil nil ("Issue1064.agda" . 56)) '(60 65 (keyword) t) '(66 67 (field) nil nil ("Issue1064.agda" . 66)) '(68 69 (symbol) t) '(70 71 (datatype) nil nil ("Issue1064.agda" . 6)))
(agda2-highlight-add-annotations 'nil '(80 82 (record) nil nil ("Issue1064.agda" . 80)) '(83 84 (symbol) t) '(85 88 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(73 79 (keyword) t) '(80 82 (record) nil nil ("Issue1064.agda" . 80)) '(89 94 (keyword) t) '(97 108 (keyword) t) '(111 122 (keyword) t) '(123 124 (coinductiveconstructor) nil nil ("Issue1064.agda" . 123)) '(127 132 (keyword) t) '(133 134 (field) nil nil ("Issue1064.agda" . 133)) '(135 136 (symbol) t) '(137 139 (record) nil nil ("Issue1064.agda" . 80)))
(agda2-highlight-add-annotations 'nil '(141 142 (function) nil nil ("Issue1064.agda" . 141)) '(143 144 (symbol) t) '(145 146 (record) nil nil ("Issue1064.agda" . 28)) '(147 148 (symbol) t) '(149 150 (datatype) nil nil ("Issue1064.agda" . 6)))
(agda2-highlight-add-annotations 'nil '(141 142 (function) nil nil ("Issue1064.agda" . 141)) '(151 152 (function) nil nil ("Issue1064.agda" . 141)) '(153 154 (bound) nil nil ("Issue1064.agda" . 153)) '(155 156 (symbol) t) '(157 160 (keyword) t) '(161 162 (inductiveconstructor) nil nil ("Issue1064.agda" . 56)) '(163 164 (bound) nil nil ("Issue1064.agda" . 163)) '(165 166 (symbol) t) '(167 168 (bound) nil nil ("Issue1064.agda" . 153)) '(169 171 (keyword) t) '(172 173 (bound) nil nil ("Issue1064.agda" . 163)))
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
