git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/interactive018/expected.out
20 lines 521 B history raw
11 : Integer
2top_private : a -> a
31 : Integer
4top_visible : a -> a
5No such variable imported1_private
6No such variable imported1_private
71 : Integer
8imported1_visible : a -> a
9No such variable imported2_private
10No such variable imported2_private
11No such variable imported2_visible
12No such variable imported2_visible
13No such variable public1_private
14No such variable public1_private
151 : Integer
16public1_visible : a -> a
17No such variable public2_private
18No such variable public2_private
191 : Integer
20public2_visible : a -> a