mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-22 19:21:39 +03:00
16 lines
338 B
Plaintext
16 lines
338 B
Plaintext
1/1: Building Issue2769 (Issue2769.idr)
|
|
Error: Issue2769.SomeRecord is already defined.
|
|
|
|
Issue2769:3:1--5:14
|
|
3 | record SomeRecord where
|
|
4 | constructor SomeRecord
|
|
5 | field : Int
|
|
|
|
1/1: Building Issue2769b (Issue2769b.idr)
|
|
Error: Main.Bar is already defined.
|
|
|
|
Issue2769b:5:1--6:18
|
|
5 | interface Blah where
|
|
6 | constructor Bar
|
|
|