(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Nat ?1 : Nat ?2 : Nat ?3 : Nat ?4 : Nat ?5 : Nat ?6 : Nat ?7 : String ?8 : String ?9 : String " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6 7 8 9)))
(agda2-give-action 0 "5")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Nat ?2 : Nat ?3 : Nat ?4 : Nat ?5 : Nat ?6 : Nat ?7 : String ?8 : String ?9 : String " nil)
((last . 1) . (agda2-goals-action '(1 2 3 4 5 6 7 8 9)))
(agda2-give-action 1 "5")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?2 : Nat ?3 : Nat ?4 : Nat ?5 : Nat ?6 : Nat ?7 : String ?8 : String ?9 : String " nil)
((last . 1) . (agda2-goals-action '(2 3 4 5 6 7 8 9)))
(agda2-give-action 2 "2 + 3")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?3 : Nat ?4 : Nat ?5 : Nat ?6 : Nat ?7 : String ?8 : String ?9 : String " nil)
((last . 1) . (agda2-goals-action '(3 4 5 6 7 8 9)))
(agda2-give-action 3 "? + ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : Nat ?5 : Nat ?6 : Nat ?7 : String ?8 : String ?9 : String ?10 : Nat ?11 : Nat " nil)
((last . 1) . (agda2-goals-action '(10 11 4 5 6 7 8 9)))
(agda2-give-action 5 "7")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : Nat ?6 : Nat ?7 : String ?8 : String ?9 : String ?10 : Nat ?11 : Nat " nil)
((last . 1) . (agda2-goals-action '(10 11 4 6 7 8 9)))
(agda2-give-action 6 "7")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : Nat ?7 : String ?8 : String ?9 : String ?10 : Nat ?11 : Nat " nil)
((last . 1) . (agda2-goals-action '(10 11 4 7 8 9)))
(agda2-give-action 7 "\"helloλ\"")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : Nat ?8 : String ?9 : String ?10 : Nat ?11 : Nat " nil)
((last . 1) . (agda2-goals-action '(10 11 4 8 9)))
(agda2-give-action 8 "primStringFromList ('h' ∷ 'e' ∷ 'l' ∷ 'l' ∷ 'o' ∷ 'λ' ∷ [])")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : Nat ?9 : String ?10 : Nat ?11 : Nat " nil)
((last . 1) . (agda2-goals-action '(10 11 4 9)))
(agda2-give-action 10 "11")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : Nat ?9 : String ?11 : Nat " nil)
((last . 1) . (agda2-goals-action '(11 4 9)))
(agda2-give-action 9 "\"['h']['i']\"")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : Nat ?11 : Nat " nil)
((last . 1) . (agda2-goals-action '(11 4)))
(agda2-give-action 11 "19")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : Nat " nil)
((last . 1) . (agda2-goals-action '(4)))
