From #4, it seems that the input mode is taken from Agda wholesale.
I will argue the removal of Agda/Juvix input mode base on the following bases
In comment 1 of #4 it seems that the mode is taken wholesale from agda with no changes.
Juvix does not require unicode input
Agda-input-mode is a minor mode, and can be enabled from any mode
For point 3. I do know people who use agda-input-mode from outside of agda for general unicode input. People likewise for Juvix-input-mode can do the same if it's so desired. Since point 1. indicates no changes are had, the user could just use agda-input-mode when they are in juvix-mode to achieve the same effect.
For point 2. there is no need for unicode for writing Juvix, Unicode symbols are open to be written, but that's the same for any programming language (even more so for languages which are simpler syntax wise due to the acceptance of more valid symbols). If a user wants to learn to use Agda's input mode, then that's good for them, but seems like a needless edition to have in the base mode. You can offer juvix-input-mode as an extra package if 1. does not hold, and you could encourage users to use it, however since the standard library lacks unicode, libraries will also follow suit, as they would look more built in. (Good design is when user extensions look like what is built in, thus libraries won't likely rock the boat given they would look like they are not built in).
Overall for these three points, I think it would be best to remove the input mode entirely
From #4, it seems that the input mode is taken from Agda wholesale.
I will argue the removal of Agda/Juvix input mode base on the following bases
For point
3.I do know people who useagda-input-modefrom outside of agda for general unicode input. People likewise forJuvix-input-modecan do the same if it's so desired. Since point1.indicates no changes are had, the user could just useagda-input-modewhen they are injuvix-modeto achieve the same effect.For point
2.there is no need for unicode for writing Juvix, Unicode symbols are open to be written, but that's the same for any programming language (even more so for languages which are simpler syntax wise due to the acceptance of more valid symbols). If a user wants to learn to use Agda's input mode, then that's good for them, but seems like a needless edition to have in the base mode. You can offerjuvix-input-modeas an extra package if1.does not hold, and you could encourage users to use it, however since the standard library lacks unicode, libraries will also follow suit, as they would look more built in. (Good design is when user extensions look like what is built in, thus libraries won't likely rock the boat given they would look like they are not built in).Overall for these three points, I think it would be best to remove the input mode entirely