(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : A ?1 : A ?2 : A → A ?3 : A ?4 : A ?5 : A ?6 : A ?7 : A → A " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6 7)))
(agda2-give-action 0 "? + x")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : A ?2 : A → A ?3 : A ?4 : A ?5 : A ?6 : A ?7 : A → A ?8 : A " nil)
((last . 1) . (agda2-goals-action '(8 1 2 3 4 5 6 7)))
(agda2-give-action 1 "x + ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?2 : A → A ?3 : A ?4 : A ?5 : A ?6 : A ?7 : A → A ?8 : A ?9 : A " nil)
((last . 1) . (agda2-goals-action '(8 9 2 3 4 5 6 7)))
(agda2-give-action 2 "_+ x")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?3 : A ?4 : A ?5 : A ?6 : A ?7 : A → A ?8 : A ?9 : A " nil)
((last . 1) . (agda2-goals-action '(8 9 3 4 5 6 7)))
(agda2-give-action 3 "? + x")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : A ?5 : A ?6 : A ?7 : A → A ?8 : A ?9 : A ?10 : A " nil)
((last . 1) . (agda2-goals-action '(8 9 10 4 5 6 7)))
(agda2-give-action 4 "? + x")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?5 : A ?6 : A ?7 : A → A ?8 : A ?9 : A ?10 : A ?12 : A " nil)
((last . 1) . (agda2-goals-action '(8 9 10 11 12 5 6 7)))
(agda2-give-action 5 "(λ a → a + (a + x)) ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?6 : A ?7 : A → A ?8 : A ?9 : A ?10 : A ?12 : A ?13 : A " nil)
((last . 1) . (agda2-goals-action '(8 9 10 11 12 13 6 7)))
(agda2-give-action 6 "x + (y + ?)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?7 : A → A ?8 : A ?9 : A ?10 : A ?12 : A ?13 : A ?14 : A " nil)
((last . 1) . (agda2-goals-action '(8 9 10 11 12 13 14 7)))
(agda2-give-action 7 "λ b → ? + b")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?8 : A ?9 : A ?10 : A ?12 : A ?13 : A ?14 : A ?15 : A " nil)
((last . 1) . (agda2-goals-action '(8 9 10 11 12 13 14 15)))
