search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Perhaps Agda.Prim should be called Agda.Primitives #963

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From nils.anders.danielsson on November 14, 2013 19:31:38

What's the reason for giving Agda.Prim an abbreviated name? I suggest that we use the name Agda.Primitives instead. (Or possibly something like Agda.Builtins.)

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

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 14, 2013 17:00:26

Ah, why didn't you complain when we discussed this at the first Agda summit? ;-)

I think Agda.Prim is in reference to GHC.Prim which I do not care about.

Agda.Primitive

would probably be a better choice then Agda.Prim (note: without the plural-s).

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 15, 2013 03:03:43

Agda.Primitive sounds good to me. In fact that's what it's called now. Please update the standard library.

Status: Accepted
Owner: nils.anders.danielsson

UlfNorell commented 10 years ago

From nils.anders.danielsson on November 15, 2013 06:09:14

Status: Fixed