(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(2 8 (keyword) t) '(18 23 (keyword) t) '(27 28 (symbol) t) '(29 32 (primitivetype) t) '(35 36 (symbol) t) '(37 38 (symbol) t) '(46 47 (symbol) t) '(48 51 (primitivetype) t) '(58 59 (symbol) t) '(60 63 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(2 8 (keyword) t) '(9 17 (module) nil nil ("Issue157.agda" . 1)) '(18 23 (keyword) t) '(25 26 (function) nil nil ("Issue157.agda" . 25)) '(33 34 (function) nil nil ("Issue157.agda" . 25)) '(40 45 (function) nil nil ("Issue157.agda" . 40)) '(52 57 (function) nil nil ("Issue157.agda" . 40)))
(agda2-highlight-add-annotations 'nil '(25 26 (function) nil nil ("Issue157.agda" . 25)) '(27 28 (symbol) t) '(29 32 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(25 26 (function) nil nil ("Issue157.agda" . 25)) '(33 34 (function) nil nil ("Issue157.agda" . 25)) '(35 36 (symbol) t) '(37 38 (symbol) t))
(agda2-info-action "*Error*" "Issue157.agda:8,9-12 Set₁ != Set when checking that the expression Set has type Set" nil)
((last . 3) . (agda2-maybe-goto '("Issue157.agda" . 60)))
(agda2-highlight-add-annotations 'nil '(37 38 (unsolvedmeta)) '(60 63 (error) nil "Issue157.agda:8,9-12 Set₁ != Set when checking that the expression Set has type Set"))
(agda2-status-action "")
