mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-19 19:01:44 +03:00
c458957bd6
Fixes #132. When getting the names in the block, we need to return the fully explicit name, because we can't assume they'll all be in the same namespace as we can have namespaces inside parameters blocks.
5 lines
188 B
Plaintext
5 lines
188 B
Plaintext
1/1: Building param (param.idr)
|
|
1/1: Building parambad (parambad.idr)
|
|
parambad.idr:7:7--8:1:While processing right hand side of Main.U at parambad.idr:7:3--8:1:
|
|
Name Main.X.foo is private
|