Improve interactive018.
Have the visible definitions refer to the private definitions to give
more confidence that evaluation doesn't get stuck.
commit319166c1b30def0991c535f91757a42e2a75f15e
authorSteven Shaw <steven@steshaw.org>
dateFri 8 Sep 2017, 19:46 (9 years ago)
parent8f6f9af
test/interactive018/Imported1.idr+2−2
@@ -3,8 +3,8 @@ module Imported1
33import Imported2
44
55imported1_private : a -> a
6−imported1_private a = a
6+imported1_private = imported2_visible
77
88export
99imported1_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
77
88export
99public1_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
55
66export
77public2_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
44import public Public1
55
66top_private : a -> a
7−top_private a = a
7+top_private = imported1_visible
88
99export
1010top_visible : a -> a
11−top_visible a = a
11+top_visible = public2_visible