git.iko.soy/Idris-dev
on master help sign in
Add (broken) test case for "private functions"
f047221Steven Shaw
test/TestData.hs+2−1
compare with master
unifiedsplit
@@ -158,7 +158,8 @@ testFamiliesData = [
158 ( 14, C_CG ),
158 ( 14, C_CG ),
159 ( 15, ANY ),
159 ( 15, ANY ),
160 ( 16, ANY ),
160 ( 16, ANY ),
161− ( 17, ANY )]),
161+ ( 17, ANY ),
162+ ( 18, ANY )]),
162 ("interfaces", "Interfaces",
163 ("interfaces", "Interfaces",
163 [ ( 1, ANY ),
164 [ ( 1, ANY ),
164 ( 2, ANY ),
165 ( 2, ANY ),
test/interactive018/Bar.idrnew file+10
@@ -0,0 +1,10 @@
1+module Bar
2+
3+import Foo
4+
5+bar_private : Nat -> Nat
6+bar_private n = n
7+
8+export
9+bar_visible : Nat -> Nat
10+bar_visible n = n
test/interactive018/Foo.idrnew file+8
@@ -0,0 +1,8 @@
1+module Foo
2+
3+foo_private : Nat -> Nat
4+foo_private n = n
5+
6+export
7+foo_visible : Nat -> Nat
8+foo_visible n = n
test/interactive018/expectednew file+4
@@ -0,0 +1,4 @@
1+bar_private : Nat -> Nat
2+bar_visible : Nat -> Nat
3+No such variable foo_private
4+foo_visible : Nat -> Nat
test/interactive018/inputnew file+4
@@ -0,0 +1,4 @@
1+:t bar_private
2+:t bar_visible
3+:t foo_private
4+:t foo_visible
test/interactive018/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --quiet --port none Bar.idr < input
3+rm -f *.ibc