Closed UlfNorell closed 10 years ago
From andres.s...@gmail.com on November 02, 2013 20:09:15
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.
From ulf.nor...@gmail.com on November 02, 2013 23:25:08
It's not actually imported, it's just loaded. The only effect of this change is that you can no longer write your own level builtin declarations. This is a good thing, since levels really are primitive and it was always a bit awkward having to worry about primLevel not being defined. I have a hard time seeing a case where you'd want to disable this.
Labels: -Priority-Medium Priority-High
From andres.s...@gmail.com on November 05, 2013 11:02:38
I have a hard time seeing a case where you'd want to disable this.
I was thinking that Agda.prim doesn't work with --no-universe-polymorphism, but I realised that this is false.
From nils.anders.danielsson on November 06, 2013 06:16:04
Status: Fixed
From andreas....@gmail.com on November 03, 2013 00:55:29
Here is a patch to remove the level builtins from Level.Agda. This patch is necessary for the latest darcs version.
Attachment: LevelToAgdaPrim.patch
Original issue: http://code.google.com/p/agda/issues/detail?id=934