git.iko.soy/Idris-dev
on master help sign in
Add test from the pull request for Elab.tryCatch
9fc97f9David Christiansen
test/meta003/Catch.idrnew file+17
compare with master
unifiedsplit
@@ -0,0 +1,17 @@
1+import Language.Reflection.Elab
2+
3+%language ElabReflection
4+
5+f : Err -> Elab ()
6+f (Msg _) = fill `("message error")
7+f (CantUnify _ _ _ _ _ _) = fill `("unification error")
8+f _ = fill `("other")
9+
10+s1 : String
11+s1 = %runElab (do tryCatch (fail []) f ; solve)
12+
13+s2 : String
14+s2 = %runElab (do tryCatch (fill `(True)) f ; solve)
15+
16+main : IO ()
17+main = do putStrLn s1 ; putStrLn s2
test/meta003/expected+2
@@ -8,3 +8,5 @@ Type mismatch between
8and
8and
9 String
9 String
10
10
11+message error
12+unification error
test/meta003/run+3−1
@@ -1,3 +1,5 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2${IDRIS:-idris} $@ --nocolour --check --consolewidth 70 BadDef.idr
2${IDRIS:-idris} $@ --nocolour --check --consolewidth 70 BadDef.idr
3+${IDRIS:-idris} $@ --nocolour --consolewidth 70 -o meta003 Catch.idr
4+./meta003
3−rm -f *.ibc
5+rm -f meta003 *.ibc