git.iko.soy/Idris-dev
on master help sign in
Add unique002 test
120b1c3Edwin Brady
test/unique002/expectednew file+2
compare with master
unifiedsplit
@@ -0,0 +1,2 @@
1+unique002.idr:15:5:Unique name xs is used more than once
2+unique002a.idr:15:5:Unique name xs is used more than once
test/unique002/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ unique002.idr --check
3+idris $@ unique002a.idr --check
4+rm -f *.ibc
test/unique002/unique002.idrnew file+20
@@ -0,0 +1,20 @@
1+data UList : Type -> UniqueType where
2+ Nil : UList a
3+ (::) : a -> UList a -> UList a
4+
5+free : {a : UniqueType} -> a -> String
6+free xs = ""
7+
8+showU : Show a => Borrowed (UList a) -> String
9+showU xs = "[" ++ showU' xs ++ "]" where
10+ showU' : Borrowed (UList a) -> String
11+ showU' [] = ""
12+ showU' (x :: xs) = show x ++ ", " ++ showU xs
13+
14+foo : UList Int -> IO ()
15+foo xs = do -- let f = \x : Int => showU xs
16+ putStrLn $ free xs
17+ putStrLn $ f 42
18+ return ()
19+ where f : Int -> String
20+ f x = showU xs
test/unique002/unique002a.idrnew file+18
@@ -0,0 +1,18 @@
1+data UList : Type -> UniqueType where
2+ Nil : UList a
3+ (::) : a -> UList a -> UList a
4+
5+free : {a : UniqueType} -> a -> String
6+free xs = ""
7+
8+showU : Show a => Borrowed (UList a) -> String
9+showU xs = "[" ++ showU' xs ++ "]" where
10+ showU' : Borrowed (UList a) -> String
11+ showU' [] = ""
12+ showU' (x :: xs) = show x ++ ", " ++ showU xs
13+
14+foo : UList Int -> IO ()
15+foo xs = do let f = \x : Int => showU xs
16+ putStrLn $ free xs
17+ putStrLn $ f 42
18+ return ()