Merge remote-tracking branch 'maint-2.4.2/maint-2.4.2'

test/interaction/Auto-BasicLogic.out

@@ -1,4 +1,4 @@
-Agda2> (agda2-status-action "")
+(agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-info-action "*Type-checking*" "Checking Auto-BasicLogic (Auto-BasicLogic.agda). " t)
@@ -8,68 +8,67 @@ Agda2> (agda2-status-action "")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?0 : (A : Set) → A → A ?1 : (A B : Set) → A → (A → B) → B ?2 : (A B : Set) → A ∧ B → B ∧ A ?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C) ?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 0 "λ A z → z")
+(agda2-give-action 0 "λ A z → z")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?1 : (A B : Set) → A → (A → B) → B ?2 : (A B : Set) → A ∧ B → B ∧ A ?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C) ?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 1 "λ A B z z₁ → z₁ z")
+(agda2-give-action 1 "λ A B z z₁ → z₁ z")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?2 : (A B : Set) → A ∧ B → B ∧ A ?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C) ?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 2 "λ A B z → ∧-i (_∧_.snd z) (_∧_.fst z)")
+(agda2-give-action 2 "λ A B z → ∧-i (_∧_.snd z) (_∧_.fst z)")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C) ?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(3 4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 3 "λ A B C z → ∧-i (_∧_.fst (_∧_.fst z)) (∧-i (_∧_.snd (_∧_.fst z)) (_∧_.snd z))")
+(agda2-give-action 3 "λ A B C z → ∧-i (_∧_.fst (_∧_.fst z)) (∧-i (_∧_.snd (_∧_.fst z)) (_∧_.snd z))")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> ((last . 2) . (agda2-make-case-action '("h4 A B C (∨-i₁ x) h₁ h₂ = h₁ x" "h4 A B C (∨-i₂ x) h₁ h₂ = h₂ x")))
+((last . 2) . (agda2-make-case-action '("h4 A B C (∨-i₁ x) h₁ h₂ = h₁ x" "h4 A B C (∨-i₂ x) h₁ h₂ = h₂ x")))
 ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> ((last . 2) . (agda2-make-case-action '("h5 A B (∨-i₁ x) = ∨-i₂ x" "h5 A B (∨-i₂ x) = ∨-i₁ x")))
+((last . 2) . (agda2-make-case-action '("h5 A B (∨-i₁ x) = ∨-i₂ x" "h5 A B (∨-i₂ x) = ∨-i₁ x")))
 ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> ((last . 2) . (agda2-make-case-action '("h6 A B C (∨-i₁ (∨-i₁ x)) = ∨-i₁ x" "h6 A B C (∨-i₁ (∨-i₂ x)) = ∨-i₂ (∨-i₁ x)" "h6 A B C (∨-i₂ x) = ∨-i₂ (∨-i₂ x)")))
+((last . 2) . (agda2-make-case-action '("h6 A B C (∨-i₁ (∨-i₁ x)) = ∨-i₁ x" "h6 A B C (∨-i₁ (∨-i₂ x)) = ∨-i₂ (∨-i₁ x)" "h6 A B C (∨-i₂ x) = ∨-i₂ (∨-i₂ x)")))
 ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> ((last . 2) . (agda2-make-case-action '("h7 A ()")))
+((last . 2) . (agda2-make-case-action '("h7 A ()")))
 ((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 8 "λ A z z₁ → z₁ z")
+(agda2-give-action 8 "λ A z z₁ → z₁ z")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 9 10 11 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 9 "λ A z z₁ → z (λ z₂ → z₂ z₁)")
+(agda2-give-action 9 "λ A z z₁ → z (λ z₂ → z₂ z₁)")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 10 11 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 10 "λ z A → z (A ∨ ((x : A) → ⊥)) (λ z₁ → z₁ (∨-i₂ (λ x → z₁ (∨-i₁ x))))")
+(agda2-give-action 10 "λ z A → z (A ∨ ((x : A) → ⊥)) (λ z₁ → z₁ (∨-i₂ (λ x → z₁ (∨-i₁ x))))")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 11 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 11 "λ z A z₁ → ∨-e A ((x : A) → ⊥) A (z A) (λ z₂ → z₂) (λ z₂ → ⊥-e A (z₁ z₂))")
+(agda2-give-action 11 "λ z A z₁ → ∨-e A ((x : A) → ⊥) A (z A) (λ z₂ → z₂) (λ z₂ → ⊥-e A (z₁ z₂))")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 12 13 14 15 16 17)))
-Agda2> (agda2-give-action 12 "λ {X} {P} {Q} z → ∧-i (λ x → _∧_.fst (z x)) (λ x → _∧_.snd (z x))")
+(agda2-give-action 12 "λ {X} {P} {Q} z → ∧-i (λ x → _∧_.fst (z x)) (λ x → _∧_.snd (z x))")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 13 14 15 16 17)))
-Agda2> (agda2-give-action 13 "λ {X} {P} {Q} z x → ∧-i (_∧_.fst z x) (_∧_.snd z x)")
+(agda2-give-action 13 "λ {X} {P} {Q} z x → ∧-i (_∧_.fst z x) (_∧_.snd z x)")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?14 : {X : Set} → X → Σ X (λ x → ⊤) ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 14 15 16 17)))
-Agda2> (agda2-give-action 14 "λ {X} x → Σ-i x (record {})")
+(agda2-give-action 14 "λ {X} x → Σ-i x (record {})")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?15 : {X : Set} → Σ (X → X) (λ x → ⊤) ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 15 16 17)))
-Agda2> (agda2-give-action 15 "λ {X} → Σ-i (λ x → x) (record {})")
+(agda2-give-action 15 "λ {X} → Σ-i (λ x → x) (record {})")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 16 17)))
-Agda2> (agda2-give-action 16 "λ {X} {P} → Σ-i (λ x → x) (λ x x₁ → x₁)")
+(agda2-give-action 16 "λ {X} {P} → Σ-i (λ x → x) (λ x x₁ → x₁)")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7 17)))
-Agda2> (agda2-give-action 17 "RAA (Σ A (λ z → (x : Drink z) → Π A Drink)) (λ z → z (Σ-i a (λ x → fun (λ a₁ → RAA (Drink a₁) (λ z₁ → z (Σ-i a₁ (λ x₁ → fun (λ a₂ → RAA (Drink a₂) (λ _ → z₁ x₁)))))))))")
+(agda2-give-action 17 "RAA (Σ A (λ z → (x : Drink z) → Π A Drink)) (λ z → z (Σ-i a (λ x → fun (λ a₁ → RAA (Drink a₁) (λ z₁ → z (Σ-i a₁ (λ x₁ → fun (λ a₂ → RAA (Drink a₂) (λ _ → z₁ x₁)))))))))")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A " nil)
 ((last . 1) . (agda2-goals-action '(4 5 6 7)))
-Agda2> Agda2> 

test/interaction/Auto-DataConstruction.out

@@ -1,4 +1,4 @@
-Agda2> (agda2-status-action "")
+(agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-info-action "*Type-checking*" "Checking Auto-DataConstruction (Auto-DataConstruction.agda). " t)
@@ -8,7 +8,6 @@ Agda2> (agda2-status-action "")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?0 : {X : Set} (xs ys : List X) → (xs ++ ys) ≡ (ys ++ xs) " nil)
 ((last . 1) . (agda2-goals-action '(0)))
-Agda2> (agda2-status-action "")
+(agda2-status-action "")
 (agda2-info-action "*Auto*" "Listing disproof(s) 0-0 0 (suc zero ∷ []) (zero ∷ []) (λ ()) " nil)
 ((last . 1) . (agda2-goals-action '(0)))
-Agda2> Agda2> 

test/interaction/Auto-EqualityReasoning.out

@@ -1,4 +1,4 @@
-Agda2> (agda2-status-action "")
+(agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-info-action "*Type-checking*" "Checking Auto-EqualityReasoning (Auto-EqualityReasoning.agda). " t)
@@ -8,8 +8,7 @@ Agda2> (agda2-status-action "")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?0 : (n + succ m) ≡ succ (n + m) ?1 : (n + m) ≡ (m + n) " nil)
 ((last . 1) . (agda2-goals-action '(0 1)))
-Agda2> ((last . 2) . (agda2-make-case-action '("lemma zero m = refl" "lemma (succ x) m = cong succ (lemma x m)")))
+((last . 2) . (agda2-make-case-action '("lemma zero m = refl" "lemma (succ x) m = cong succ (lemma x m)")))
 ((last . 1) . (agda2-goals-action '(0 1)))
-Agda2> ((last . 2) . (agda2-make-case-action '("addcommut zero zero = refl" "addcommut zero (succ x) = sym (cong succ (addcommut x zero))" "addcommut (succ x) m = begin (succ (x + m) ≡⟨ cong succ (addcommut x m) ⟩ (succ (m + x) ≡⟨ sym (lemma' m x) ⟩ ((m + succ x) ∎)))")))
+((last . 2) . (agda2-make-case-action '("addcommut zero zero = refl" "addcommut zero (succ x) = sym (cong succ (addcommut x zero))" "addcommut (succ x) m = begin (succ (x + m) ≡⟨ cong succ (addcommut x m) ⟩ (succ (m + x) ≡⟨ sym (lemma' m x) ⟩ ((m + succ x) ∎)))")))
 ((last . 1) . (agda2-goals-action '(0 1)))
-Agda2> Agda2> 

test/interaction/Auto-IndexedDatatypes.out

@@ -1,4 +1,4 @@
-Agda2> (agda2-status-action "")
+(agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-info-action "*Type-checking*" "Checking Auto-IndexedDatatypes (Auto-IndexedDatatypes.agda). " t)
@@ -8,22 +8,21 @@ Agda2> (agda2-status-action "")
 (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)))
-Agda2> ((last . 2) . (agda2-make-case-action '("h0 {zero} = even-0" "h0 {succ x} = even-s (odd-s h0)")))
+((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)))
-Agda2> ((last . 2) . (agda2-make-case-action '("map f [] = []" "map f (x ∷ x₁) = f x ∷ map f x₁")))
+((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)))
-Agda2> ((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 . 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> (agda2-give-action 3 "eval σ e (eval σ e₁)")
+(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> (agda2-give-action 4 "lookup' x σ")
+(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> (agda2-give-action 5 "eval (cons x σ) e")
+(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)))
-Agda2> Agda2> 

test/interaction/Auto-Misc.out

@@ -1,4 +1,4 @@
-Agda2> (agda2-status-action "")
+(agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-info-action "*Type-checking*" "Checking Auto-Misc (Auto-Misc.agda). " t)
@@ -8,16 +8,15 @@ Agda2> (agda2-status-action "")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?0 : (x₁ x₂ : ⊥) → x₁ ≡ x₂ ?1 : .B ?2 : .A " nil)
 ((last . 1) . (agda2-goals-action '(0 1 2)))
-Agda2> (agda2-give-action 0 "λ x₁ → λ ()")
+(agda2-give-action 0 "λ x₁ → λ ()")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?1 : .B ?2 : .A " nil)
 ((last . 1) . (agda2-goals-action '(1 2)))
-Agda2> (agda2-give-action 1 "(Σ.prf h)")
+(agda2-give-action 1 "(Σ.prf h)")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?2 : .A " nil)
 ((last . 1) . (agda2-goals-action '(2)))
-Agda2> (agda2-give-action 2 "(Σ.wit h)")
+(agda2-give-action 2 "(Σ.wit h)")
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "" nil)
 ((last . 1) . (agda2-goals-action '()))
-Agda2> Agda2>