(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(1 4 (symbol) t) '(5 12 (keyword) t) '(13 26 (pragma) t) '(27 30 (symbol) t) '(32 36 (keyword) t) '(39 40 (symbol) t) '(45 50 (keyword) t) '(52 58 (keyword) t) '(61 62 (symbol) t) '(67 72 (keyword) t) '(75 86 (keyword) t) '(91 96 (keyword) t) '(99 100 (symbol) t) '(104 110 (keyword) t) '(114 115 (symbol) t) '(120 125 (keyword) t) '(128 139 (keyword) t) '(142 153 (keyword) t) '(158 163 (keyword) t) '(166 167 (symbol) t) '(174 175 (symbol) t) '(178 179 (symbol) t) '(186 187 (symbol) t) '(188 191 (keyword) t) '(196 197 (symbol) t) '(200 202 (keyword) t))
(agda2-highlight-add-annotations 'nil '(37 38 (datatype) nil nil ("Issue1064.agda" . 37)) '(41 44 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(59 60 (record) nil nil ("Issue1064.agda" . 59)) '(63 66 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(87 88 (inductiveconstructor) nil nil ("Issue1064.agda" . 87)) '(97 98 (field) nil nil ("Issue1064.agda" . 97)) '(101 102 (datatype) nil nil ("Issue1064.agda" . 37)) '(111 113 (record) nil nil ("Issue1064.agda" . 111)) '(116 119 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(154 155 (coinductiveconstructor) nil nil ("Issue1064.agda" . 154)) '(164 165 (field) nil nil ("Issue1064.agda" . 164)) '(168 170 (record) nil nil ("Issue1064.agda" . 111)) '(172 173 (function) nil nil ("Issue1064.agda" . 172)) '(176 177 (record) nil nil ("Issue1064.agda" . 59)) '(180 181 (datatype) nil nil ("Issue1064.agda" . 37)) '(182 183 (function) nil nil ("Issue1064.agda" . 172)) '(184 185 (bound) nil nil ("Issue1064.agda" . 184)) '(192 193 (inductiveconstructor)) '(194 195 (bound) nil nil ("Issue1064.agda" . 194)) '(198 199 (bound) nil nil ("Issue1064.agda" . 184)) '(203 204 (bound) nil nil ("Issue1064.agda" . 194)))
(agda2-highlight-add-annotations 'nil '(37 38 (datatype) nil nil ("Issue1064.agda" . 37)) '(39 40 (symbol) t) '(41 44 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(32 36 (keyword) t) '(37 38 (datatype) nil nil ("Issue1064.agda" . 37)) '(45 50 (keyword) t))
(agda2-highlight-add-annotations 'nil '(59 60 (record) nil nil ("Issue1064.agda" . 59)) '(61 62 (symbol) t) '(63 66 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(52 58 (keyword) t) '(59 60 (record) nil nil ("Issue1064.agda" . 59)) '(67 72 (keyword) t) '(75 86 (keyword) t) '(87 88 (inductiveconstructor) nil nil ("Issue1064.agda" . 87)) '(91 96 (keyword) t) '(97 98 (field) nil nil ("Issue1064.agda" . 97)) '(99 100 (symbol) t) '(101 102 (datatype) nil nil ("Issue1064.agda" . 37)))
(agda2-highlight-add-annotations 'nil '(111 113 (record) nil nil ("Issue1064.agda" . 111)) '(114 115 (symbol) t) '(116 119 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(104 110 (keyword) t) '(111 113 (record) nil nil ("Issue1064.agda" . 111)) '(120 125 (keyword) t) '(128 139 (keyword) t) '(142 153 (keyword) t) '(154 155 (coinductiveconstructor) nil nil ("Issue1064.agda" . 154)) '(158 163 (keyword) t) '(164 165 (field) nil nil ("Issue1064.agda" . 164)) '(166 167 (symbol) t) '(168 170 (record) nil nil ("Issue1064.agda" . 111)))
(agda2-highlight-add-annotations 'nil '(172 173 (function) nil nil ("Issue1064.agda" . 172)) '(176 177 (record) nil nil ("Issue1064.agda" . 59)) '(180 181 (datatype) nil nil ("Issue1064.agda" . 37)))
(agda2-highlight-add-annotations 'nil '(172 173 (function) nil nil ("Issue1064.agda" . 172)) '(182 183 (function) nil nil ("Issue1064.agda" . 172)) '(184 185 (bound) nil nil ("Issue1064.agda" . 184)) '(186 187 (symbol) t) '(188 191 (keyword) t) '(192 193 (inductiveconstructor) nil nil ("Issue1064.agda" . 87)) '(194 195 (bound) nil nil ("Issue1064.agda" . 194)) '(196 197 (symbol) t) '(198 199 (bound) nil nil ("Issue1064.agda" . 184)) '(200 202 (keyword) t) '(203 204 (bound) nil nil ("Issue1064.agda" . 194)))
(agda2-highlight-add-annotations 'nil '(1 4 (symbol) t) '(5 12 (keyword) t) '(13 26 (pragma) t) '(27 30 (symbol) t) '(174 175 (symbol) t) '(178 179 (symbol) t))
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
