Closed UlfNorell closed 10 years ago
UlfNorell
commented
10 years ago From andreas....@gmail.com on November 08, 2013 05:30:17
True, the discovering of 0 was a major breakthrough in math... The empty set of clauses is still a set of clauses.
Status: Accepted
Labels: Type-Enhancement Syntax Where
UlfNorell
commented
10 years ago From ulf.nor...@gmail.com on November 08, 2013 22:19:45
Status: Fixed
UlfNorell
commented
10 years ago From nils.anders.danielsson on November 11, 2013 05:45:46
Please document this change in the release notes.
Status: Accepted
Labels: Priority-High Milestone-2.3.4
UlfNorell
commented
10 years ago From nils.anders.danielsson on November 11, 2013 05:47:05
Oops, I saw now that you put the documentation in another patch.
Status: Fixed
Labels: -Priority-High -Milestone-2.3.4
From guillaum...@gmail.com on November 08, 2013 12:57:51
Is there a reason why the following is a syntax error?
A : Set1 A = Set where
It’s of course not very useful to have a "where" without anything after it, but sometimes I have a term M using a term N in a "where", and if for some reason I want to comment out the term N, then I need to remember to comment the keyword "where" as well, which is slightly annoying.
Original issue: http://code.google.com/p/agda/issues/detail?id=947