You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Question: Would it not be better to call the package java? As we are already in Idris, the Idris in the IdrisJava namespace seems a little redundant.
If I have time I shall make the alterations myself and issue a PR, but thought it worth a mention in case anybody agrees and wishes to contribute a PR. Also I have no idea how this would affect upstream dev..
The text was updated successfully, but these errors were encountered:
In a application I've written for automatically generating FFI interface for Java method prototypes, there is a library for Java syntax and parsing, packaged under the name Java.
Ah okay. Thought it was worth a mention. Personally, I liked the approach taken in the python backend (ziman/idris-py) where the namespace is Python a little bit cleaner.
Question: Would it not be better to call the package
java
? As we are already in Idris, the Idris in theIdrisJava
namespace seems a little redundant.If I have time I shall make the alterations myself and issue a PR, but thought it worth a mention in case anybody agrees and wishes to contribute a PR. Also I have no idea how this would affect upstream dev..
The text was updated successfully, but these errors were encountered: