search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

make library-test fails #935

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From andres.s...@gmail.com on November 03, 2013 03:58:34

$ make library-test ... Duplicate binding for built-in thing LEVEL, previous binding to .Agda.Prim.Level

I think it is not a good idea that Agda automatically imports Agda.Prim. At least, there should be an option to disable this behavior.

Original issue: http://code.google.com/p/agda/issues/detail?id=935

UlfNorell commented 10 years ago

From andres.s...@gmail.com on November 02, 2013 20:08:13

Status: Invalid
Owner: ---