mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 02:31:50 +03:00
14 lines
378 B
Plaintext
14 lines
378 B
Plaintext
1/1: Building param (param.idr)
|
|
1/1: Building parambad (parambad.idr)
|
|
Error: While processing right hand side of U. Name Main.X.foo is private.
|
|
|
|
parambad.idr:7:7--7:10
|
|
3 | foo : Bool
|
|
4 | foo = True
|
|
5 |
|
|
6 | U : Bool
|
|
7 | U = foo
|
|
^^^
|
|
|
|
Suggestion: add an explicit export or public export modifier. By default, all names are private in namespace blocks.
|