Open UlfNorell opened 10 years ago
From nils.anders.danielsson on December 02, 2013 14:38:23
It would be nice if agda --html generated readable anchors (#foldr instead of #2121).
If this is implemented, then non-ASCII names, anonymous modules, overloaded constructors and perhaps some other constructions need to be handled appropriately.
Original issue: http://code.google.com/p/agda/issues/detail?id=987
From nils.anders.danielsson on December 02, 2013 14:38:23
It would be nice if agda --html generated readable anchors (#foldr instead of #2121).
If this is implemented, then non-ASCII names, anonymous modules, overloaded constructors and perhaps some other constructions need to be handled appropriately.
Original issue: http://code.google.com/p/agda/issues/detail?id=987