idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 01:01:59 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #1236 ] Already fixed, add test case

Browse Source
This commit is contained in:
Guillaume Allais 2024-07-25 09:49:54 +01:00 committed by G. Allais
parent a65298e210
commit 1eed6a817d
3 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
tests/idris2/error/error030/Issue1236.idr Normal file
View File

@ -0,0 +1,5 @@
private
data Foo : Type
public export
data Foo : Type where

7
tests/idris2/error/error030/expected Normal file
View File

@ -0,0 +1,7 @@
1/1: Building Issue1236 (Issue1236.idr)
Warning: Main.Foo has been forward-declared with private visibility, cannot change to public export. This will be an error in a later release.
Issue1236:4:1--5:22
4 | public export
5 | data Foo : Type where

3
tests/idris2/error/error030/run Executable file
View File

@ -0,0 +1,3 @@
. ../../../testutils.sh
check Issue1236.idr