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

Merge pull request #342 from csabahruska/master

Browse Source 
add unit test for constructor duplicate
This commit is contained in:
Niklas Larsson 2020-06-25 10:39:25 +02:00 committed by GitHub
commit 8d75d70fac
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
tests/Main.idr
View File

@ -47,6 +47,7 @@ idrisTests
-- Error messages
"error001", "error002", "error003", "error004", "error005",
"error006", "error007", "error008", "error009", "error010",
"error011",
-- Modules and imports
"import001", "import002", "import003", "import004",
-- Interactive editing support

5
tests/idris2/error011/ConstructorDuplicate.idr Normal file
View File

@ -0,0 +1,5 @@
data A = B | B
data C : Type -> Type where
D : C Int
D : C String

3
tests/idris2/error011/expected Normal file
View File

@ -0,0 +1,3 @@
1/1: Building ConstructorDuplicate (ConstructorDuplicate.idr)
ConstructorDuplicate.idr:1:14--3:1:Main.B is already defined
ConstructorDuplicate.idr:5:3--5:15:Main.D is already defined

3
tests/idris2/error011/run Executable file
View File

@ -0,0 +1,3 @@
$1 ConstructorDuplicate.idr --check
rm -rf build