(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(2 8 (keyword) t) '(19 24 (keyword) t) '(26 35 (keyword) t) '(42 43 (symbol) t) '(44 47 (primitivetype) t) '(54 55 (symbol) t) '(58 59 (symbol) t) '(62 63 (symbol) t) '(64 67 (primitivetype) t) '(74 75 (symbol) t) '(76 77 (symbol) t) '(78 79 (symbol) t) '(82 83 (symbol) t) '(84 85 (symbol) t) '(92 93 (symbol) t))
(agda2-highlight-add-annotations 'nil '(2 8 (keyword) t) '(9 18 (module) nil nil ("Issue157b.agda" . 1)) '(19 24 (keyword) t) '(38 39 (postulate) nil nil ("Issue157b.agda" . 38)) '(40 41 (postulate) nil nil ("Issue157b.agda" . 40)) '(50 51 (postulate) nil nil ("Issue157b.agda" . 50)) '(56 57 (postulate) nil nil ("Issue157b.agda" . 38)) '(60 61 (postulate) nil nil ("Issue157b.agda" . 40)) '(70 73 (postulate) nil nil ("Issue157b.agda" . 70)) '(79 80 (bound) nil nil ("Issue157b.agda" . 79)) '(81 82 (bound) nil nil ("Issue157b.agda" . 81)) '(86 87 (postulate) nil nil ("Issue157b.agda" . 50)) '(88 89 (bound) nil nil ("Issue157b.agda" . 79)) '(90 91 (bound) nil nil ("Issue157b.agda" . 81)) '(94 95 (postulate) nil nil ("Issue157b.agda" . 50)) '(96 97 (bound) nil nil ("Issue157b.agda" . 81)))
(agda2-highlight-add-annotations 'nil '(38 39 (postulate) nil nil ("Issue157b.agda" . 38)) '(42 43 (symbol) t) '(44 47 (primitivetype) t))
(agda2-highlight-add-annotations 'nil '(40 41 (postulate) nil nil ("Issue157b.agda" . 40)))
(agda2-highlight-add-annotations 'nil '(50 51 (postulate) nil nil ("Issue157b.agda" . 50)) '(54 55 (symbol) t) '(56 57 (postulate) nil nil ("Issue157b.agda" . 38)) '(58 59 (symbol) t) '(60 61 (postulate) nil nil ("Issue157b.agda" . 40)) '(62 63 (symbol) t) '(64 67 (primitivetype) t))
(agda2-info-action "*Error*" "Issue157b.agda:7,27-30 B → Set should be a sort, but it isn't when checking that the inferred type of an application B → Set matches the expected type _7" nil)
((last . 3) . (agda2-maybe-goto '("Issue157b.agda" . 94)))
(agda2-highlight-add-annotations 'nil '(94 95 (error unsolvedmeta) nil "Issue157b.agda:7,27-30 B → Set should be a sort, but it isn't when checking that the inferred type of an application B → Set matches the expected type _7") '(95 96 (unsolvedmeta)) '(96 97 (error unsolvedmeta) nil "Issue157b.agda:7,27-30 B → Set should be a sort, but it isn't when checking that the inferred type of an application B → Set matches the expected type _7"))
(agda2-status-action "")
