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