(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(1 2 (missingdefinition)))
(agda2-highlight-add-annotations 'nil '(3 4 (symbol) t))
(agda2-highlight-add-annotations 'nil '(1 2 (postulate) nil nil ("HighlightMissingDefinition.agda" . 1)) '(5 8 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(1 2 (postulate) nil nil ("HighlightMissingDefinition.agda" . 1)) '(5 8 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(3 4 (symbol) t))
(agda2-status-action "")
(agda2-info-action "*All Errors*" "HighlightMissingDefinition.agda:1,1-2 The following names are declared but not accompanied by a definition: A " nil)
((last . 1) . (agda2-goals-action '()))
