[ test #2749 ] Also covering the forall case

asr · Dec 6, 2017 · 058986f · 058986f
1 parent a9020c7
commit 058986f
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 18 deletions.
diff --git a/test/interaction/Issue2749-2.agda b/test/interaction/Issue2749-2.agda
@@ -14,3 +14,9 @@ data B : Set where
 -- testing unicode suffixes
 left : B → B
 left b₁ = {!!}
+
+open import Agda.Builtin.Equality
+
+-- testing ascii only forall
+allq : (∀ m n → m ≡ n) ≡ {!!}
+allq = refl
diff --git a/test/interaction/Issue2749-2.in b/test/interaction/Issue2749-2.in
@@ -3,4 +3,5 @@ goal_command 0 (cmd_intro False) ""
 top_command (showImplicitArgs True)
 goal_command 1 cmd_make_case ""
 top_command (showImplicitArgs False)
-goal_command 2 cmd_make_case "b₁"
+goal_command 2 cmd_make_case "b₁"
+goal_command 3 (cmd_solveOne AsIs) ""
diff --git a/test/interaction/Issue2749-2.out b/test/interaction/Issue2749-2.out
@@ -2,17 +2,19 @@
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-status-action "")
-(agda2-info-action "*All Goals*" "?0 : .A → .A ?1 : .A → .A ?2 : B " nil)
-((last . 1) . (agda2-goals-action '(0 1 2)))
+(agda2-info-action "*All Goals*" "?0 : .A → .A ?1 : .A → .A ?2 : B ?3 : Set _17 Sort _17 [ at Issue2749-2.agda:21,11-12 ] _18 : Set _17 [ at Issue2749-2.agda:21,11-12 ] " nil)
+((last . 1) . (agda2-goals-action '(0 1 2 3)))
 (agda2-give-action 0 "λ x → ?")
 (agda2-status-action "")
-(agda2-info-action "*All Goals*" "?1 : .A → .A ?2 : B ?3 : .A " nil)
-((last . 1) . (agda2-goals-action '(3 1 2)))
+(agda2-info-action "*All Goals*" "?1 : .A → .A ?2 : B ?3 : Set _17 ?4 : .A Sort _17 [ at Issue2749-2.agda:21,11-12 ] _18 : Set _17 [ at Issue2749-2.agda:21,11-12 ] " nil)
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
 (agda2-status-action "ShowImplicit")
-((last . 1) . (agda2-goals-action '(3 1 2)))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
 ((last . 2) . (agda2-make-case-action '("it {A} ⦃ a ⦄ x = ?")))
-((last . 1) . (agda2-goals-action '(3 1 2)))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
 (agda2-status-action "")
-((last . 1) . (agda2-goals-action '(3 1 2)))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
 ((last . 2) . (agda2-make-case-action '("left (mkB b₁ b₂) = ?")))
-((last . 1) . (agda2-goals-action '(3 1 2)))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
+((last . 2) . (agda2-solveAll-action '(3 "∀ m n → m ≡ n")))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
diff --git a/test/interaction/Issue2749.agda b/test/interaction/Issue2749.agda
@@ -16,3 +16,9 @@ data B : Set where
 -- testing ascii only suffixes
 left : B → B
 left b1 = {!!}
+
+open import Agda.Builtin.Equality
+
+-- testing ascii only forall
+allq : (∀ m n → m ≡ n) ≡ {!!}
+allq = refl
diff --git a/test/interaction/Issue2749.in b/test/interaction/Issue2749.in
@@ -3,4 +3,5 @@ goal_command 0 (cmd_intro False) ""
 top_command (showImplicitArgs True)
 goal_command 1 cmd_make_case ""
 top_command (showImplicitArgs False)
-goal_command 2 cmd_make_case "b1"
+goal_command 2 cmd_make_case "b1"
+goal_command 3 (cmd_solveOne AsIs) ""
diff --git a/test/interaction/Issue2749.out b/test/interaction/Issue2749.out
@@ -2,17 +2,19 @@
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-status-action "")
-(agda2-info-action "*All Goals*" "?0 : .A -> .A ?1 : .A -> .A ?2 : B " nil)
-((last . 1) . (agda2-goals-action '(0 1 2)))
+(agda2-info-action "*All Goals*" "?0 : .A -> .A ?1 : .A -> .A ?2 : B ?3 : Set _17 Sort _17 [ at Issue2749.agda:23,11-12 ] _18 : Set _17 [ at Issue2749.agda:23,11-12 ] " nil)
+((last . 1) . (agda2-goals-action '(0 1 2 3)))
 (agda2-give-action 0 "\\ x -> ?")
 (agda2-status-action "")
-(agda2-info-action "*All Goals*" "?1 : .A -> .A ?2 : B ?3 : .A " nil)
-((last . 1) . (agda2-goals-action '(3 1 2)))
+(agda2-info-action "*All Goals*" "?1 : .A -> .A ?2 : B ?3 : Set _17 ?4 : .A Sort _17 [ at Issue2749.agda:23,11-12 ] _18 : Set _17 [ at Issue2749.agda:23,11-12 ] " nil)
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
 (agda2-status-action "ShowImplicit")
-((last . 1) . (agda2-goals-action '(3 1 2)))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
 ((last . 2) . (agda2-make-case-action '("it {A} {{a}} x = ?")))
-((last . 1) . (agda2-goals-action '(3 1 2)))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
 (agda2-status-action "")
-((last . 1) . (agda2-goals-action '(3 1 2)))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
 ((last . 2) . (agda2-make-case-action '("left (mkB b1 b2) = ?")))
-((last . 1) . (agda2-goals-action '(3 1 2)))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))
+((last . 2) . (agda2-solveAll-action '(3 "forall m n -> m ≡ n")))
+((last . 1) . (agda2-goals-action '(4 1 2 3)))