mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 20:23:11 +03:00
add unit test for constructor duplicate
This commit is contained in:
parent
d31e59bacf
commit
6de225e4be
@ -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
5
tests/idris2/error011/ConstructorDuplicate.idr
Normal 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
3
tests/idris2/error011/expected
Normal 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
3
tests/idris2/error011/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 ConstructorDuplicate.idr --check
|
||||
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user