mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 00:10:31 +03:00
ff7d3a0246
That is, don't generalise multiplicities, because we need the hole type to be precise wrt multiplicities. Resolves #189
9 lines
189 B
Plaintext
9 lines
189 B
Plaintext
1/1: Building Dup (Dup.idr)
|
|
Dup.idr:13:1--15:1:Main.Test is already defined
|
|
Main> Bye for now!
|
|
1/1: Building Scope (Scope.idr)
|
|
Main> Main.Test : Type
|
|
Main.X.Test : Type
|
|
Main>
|
|
Bye for now!
|