(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Even (double n) ?1 : Vec Y n ?2 : ∥ a ∥ ?3 : ∥ a ∥ ?4 : ∥ a ∥ ?5 : ∥ b ∥ " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
((last . 2) . (agda2-make-case-action '("h0 {zero} = even-0" "h0 {succ x} = even-s (odd-s h0)")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
((last . 2) . (agda2-make-case-action '("map f [] = []" "map f (x ∷ x₁) = f x ∷ map f x₁")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
((last . 2) . (agda2-make-case-action '("lookup {_} {< x >} zero (cons x₁ x₂) = x₁" "lookup {_} {< x >} (succ x₁) (cons x₂ x₃) = lookup x₁ x₃" "lookup {_} {x ⇒ x₁} zero (cons x₂ x₃) = x₂" "lookup {_} {x ⇒ x₁} (succ x₂) (cons x₃ x₄) = lookup x₂ x₄")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5)))
(agda2-give-action 3 "eval σ e (eval σ e₁)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Even (double n) ?1 : Vec Y n ?2 : ∥ a ∥ ?4 : ∥ a ∥ ?5 : ∥ b ∥ " nil)
((last . 1) . (agda2-goals-action '(0 1 2 4 5)))
(agda2-give-action 4 "lookup' x σ")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Even (double n) ?1 : Vec Y n ?2 : ∥ a ∥ ?5 : ∥ b ∥ " nil)
((last . 1) . (agda2-goals-action '(0 1 2 5)))
(agda2-give-action 5 "eval (cons x σ) e")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Even (double n) ?1 : Vec Y n ?2 : ∥ a ∥ " nil)
((last . 1) . (agda2-goals-action '(0 1 2)))
