test: Assert info window output of inferType

phijor · Jan 29, 2023 · 1172b35 · 1172b35
1 parent 6e9d5a8
commit 1172b35
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/test/Hello.agda b/test/Hello.agda
@@ -42,3 +42,5 @@ elaborate = {! 3 !}
 sub₀and-super⁹ : Nat
 sub₀and-super⁹ = 15
 
+infer : Bool → Bool → Bool
+infer x = {! x !}
diff --git a/test/TestSpec.hs b/test/TestSpec.hs
@@ -162,3 +162,11 @@ spec = focus $ do
     goto w 43 16
     incNextDigitSeq
 
+  vimSpec "should infer type of local variable" timeout "test/Hello.agda" $ \w b -> do
+    withBufferStuff b $ \bs -> do
+        goto w 46 14
+        inferType AsIs
+        liftIO $ threadDelay 5e5
+        res <- buffer_get_lines (iw_buffer $ bs_info_win bs) vimFirstLine vimLastLine False
+        liftIO $ V.toList res `shouldContain` ["Inferred Type: Bool"]
+