(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(1 7 (keyword) t) '(10 11 (symbol) t) '(17 22 (keyword) t) '(25 30 (keyword) t) '(37 38 (symbol) t) '(48 49 (symbol) t) '(58 59 (symbol) t) '(65 70 (keyword) t) '(77 78 (symbol) t) '(88 89 (symbol) t) '(98 99 (symbol) t) '(102 103 (symbol) t) '(106 107 (symbol) t))
(agda2-highlight-add-annotations 'nil '(8 9 (record) nil nil ("Issue3020.agda" . 8)) '(12 16 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(35 36 (field) nil nil ("Issue3020.agda" . 35)) '(39 42 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(46 47 (bound) nil nil ("Issue3020.agda" . 46)) '(50 53 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(56 57 (bound) nil nil ("Issue3020.agda" . 46)) '(60 61 (field) nil nil ("Issue3020.agda" . 35)) '(75 76 (field) nil nil ("Issue3020.agda" . 75)) '(79 82 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(86 87 (function) nil nil ("Issue3020.agda" . 86)) '(90 93 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(96 97 (function) nil nil ("Issue3020.agda" . 86)) '(100 101 (field) nil nil ("Issue3020.agda" . 35)) '(104 105 (function) nil nil ("Issue3020.agda" . 46)) '(108 109 (field) nil nil ("Issue3020.agda" . 75)))
(agda2-highlight-add-annotations 'nil '(8 9 (record) nil nil ("Issue3020.agda" . 8)) '(10 11 (symbol) t) '(12 16 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(1 7 (keyword) t) '(8 9 (record) nil nil ("Issue3020.agda" . 8)) '(17 22 (keyword) t) '(25 30 (keyword) t) '(35 36 (field) nil nil ("Issue3020.agda" . 35)) '(37 38 (symbol) t) '(39 42 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(46 47 (function) nil nil ("Issue3020.agda" . 46)) '(48 49 (symbol) t) '(50 53 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(56 57 (function) nil nil ("Issue3020.agda" . 46)) '(58 59 (symbol) t) '(60 61 (field) nil nil ("Issue3020.agda" . 35)) '(65 70 (keyword) t) '(75 76 (field) nil nil ("Issue3020.agda" . 75)) '(77 78 (symbol) t) '(79 82 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(86 87 (function) nil nil ("Issue3020.agda" . 86)) '(88 89 (symbol) t) '(90 93 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(96 97 (function) nil nil ("Issue3020.agda" . 86)) '(98 99 (symbol) t) '(100 101 (field) nil nil ("Issue3020.agda" . 35)) '(102 103 (symbol) t) '(104 105 (function) nil nil ("Issue3020.agda" . 46)) '(106 107 (symbol) t) '(108 109 (field) nil nil ("Issue3020.agda" . 75)))
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
