git.iko.soy/Idris-dev
on master help sign in
Improve interactive018.
319166cSteven Shaw
test/interactive018/Imported1.idr+2−2
compare with master
unifiedsplit
@@ -3,8 +3,8 @@ module Imported1
3import Imported2
3import Imported2
4
4
5imported1_private : a -> a
5imported1_private : a -> a
6−imported1_private a = a
6+imported1_private = imported2_visible
7
7
8export
8export
9imported1_visible : a -> a
9imported1_visible : a -> a
10−imported1_visible a = a
10+imported1_visible = imported1_private
test/interactive018/Public1.idr+1−1
@@ -7,4 +7,4 @@ public1_private a = a
7
7
8export
8export
9public1_visible : a -> a
9public1_visible : a -> a
10−public1_visible a = a
10+public1_visible = public1_private
test/interactive018/Public2.idr+1−1
@@ -5,4 +5,4 @@ public2_private a = a
5
5
6export
6export
7public2_visible : a -> a
7public2_visible : a -> a
8−public2_visible a = a
8+public2_visible = public2_private
test/interactive018/Top.idr+2−2
@@ -4,8 +4,8 @@ import Imported1
4import public Public1
4import public Public1
5
5
6top_private : a -> a
6top_private : a -> a
7−top_private a = a
7+top_private = imported1_visible
8
8
9export
9export
10top_visible : a -> a
10top_visible : a -> a
11−top_visible a = a
11+top_visible = public2_visible