[ test ] case for the fix

Author: gallais

tests/ideMode/ideMode005/LetBinders.idr

@@ -0,0 +1,27 @@
+module LetBinders
+
+infix 1 :::
+record List1 (a : Type) where
+  constructor (:::)
+  head : a
+  tail : List a
+
+swap : List1 a -> List1 a
+swap aas =
+  let (a ::: as) := aas in
+  let (b :: bs) = as
+        | [] => a ::: []
+      rest = a :: bs
+  in b ::: rest
+
+identity : List (Nat, a) -> List (List a)
+identity =
+  let
+
+    replicate : (n : Nat) -> a -> List a
+    replicate Z a = []
+    replicate (S n) a = a :: replicate n a
+
+    closure := uncurry replicate
+
+  in map closure

tests/ideMode/ideMode005/Syntax.idr

@@ -2,10 +2,6 @@ module Syntax
 
 %default total
 
-{- -- interfaces don't work yet
-{0 a : Type} -> (foo : Show a) => Show (Maybe a) where
--}
-
 showMaybe : {0 a : Type} -> (assumption : Show a) => Maybe a -> String
 showMaybe x@ma = case map (id . id) ma of
     Nothing => "Nothing"

tests/ideMode/ideMode005/expected1

@@ -0,0 +1 @@
+000021((:load-file "LetBinders.idr") 1)

tests/ideMode/ideMode005/expectedG

@@ -15,6 +15,7 @@ $1 --no-color --console-width 0 --ide-mode < inputC > expectedC
 $1 --no-color --console-width 0 --ide-mode < inputD > expectedD
 $1 --no-color --console-width 0 --ide-mode < inputE > expectedE
 $1 --no-color --console-width 0 --ide-mode < inputF > expectedF
+$1 --no-color --console-width 0 --ide-mode < inputG > expectedG
 
 rm -f expected output*
 touch expected

tests/ideMode/ideMode005/inputG

@@ -45,4 +45,7 @@ diff expectedE outputE >> output
 $1 --no-color --console-width 0 --ide-mode < inputF > outputF
 diff expectedF outputF >> output
 
+$1 --no-color --console-width 0 --ide-mode < inputG > outputG
+diff expectedG outputG >> output
+
 rm -rf build