AutoMisc.out

Agda2> (agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking AutoMisc (AutoMisc.agda).\n" t)
(agda2-info-action "*Type-checking*" "Finished AutoMisc.\n" t)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : (n + suc m) ≡ suc (n + m)\n?1 : (n + m) ≡ (m + n)\n?2 : Σ A (λ x → Drink x → Π A Drink)\n?3 : Vec .Y .n\n?4 : {X : Set} (xs ys : List X) → (xs ++ ys) ≡ (ys ++ xs)\n" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4)))
Agda2> ((last . 2) . (agda2-make-case-action '("lemma zero m = refl" "lemma (suc n) m = cong suc (lemma n m)")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4)))
Agda2> ((last . 2) . (agda2-make-case-action '("addcommut zero zero = refl" "addcommut zero (suc n) = sym (cong suc (addcommut n zero))" "addcommut (suc n) m = begin (suc (n + m) ≡⟨ cong suc (addcommut n m) ⟩ (suc (m + n) ≡⟨ sym (lemma' m n) ⟩ ((m + suc n) ∎)))")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4)))
Agda2> (agda2-give-action 2 "RAA (Σ A (λ z → (x : Drink z) → Π A Drink))\n(λ z →\n   z\n   (ΣI a\n    (λ x →\n       fun\n       (λ a₁ →\n          RAA (Drink a₁)\n          (λ z₁ →\n             z (ΣI a₁ (λ x₁ → fun (λ a₂ → RAA (Drink a₂) (λ _ → z₁ x₁)))))))))")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : (n + suc m) ≡ suc (n + m)\n?1 : (n + m) ≡ (m + n)\n?3 : Vec .Y .n\n?4 : {X : Set} (xs ys : List X) → (xs ++ ys) ≡ (ys ++ xs)\n" nil)
((last . 1) . (agda2-goals-action '(0 1 3 4)))
Agda2> ((last . 2) . (agda2-make-case-action '("map f [] = []" "map f (x ∷ x₁) = f x ∷ map f x₁")))
((last . 1) . (agda2-goals-action '(0 1 3 4)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Auto*" "Listing disproof(s) 0-0\n0  (suc zero ∷ []) (zero ∷ []) (λ ())\n" nil)
((last . 1) . (agda2-goals-action '(0 1 3 4)))
Agda2>