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