Unicode operators

[toastal]

I would like have the option (meaning supporting both) to use Unicode operators to mean what I type with the literal and appropriate Unicode symbols instead of having ASCII symbols approximate those Unicode symbols. Input is a solved issue (layers, compose, digraphs, etc.). I would propose all or some of:

Unicode	ASCII	description
×	*	multiplication
÷	/	division
≡	==	equal
≠	!=	not equal
≥	>=	greater or equal
≤	<=	smaller or equal
∧	&&	and
∨	||	or
¬	!	not
λ	fun	function
→	->	type-level arrow
⇒	=>	function-level arrow (?)
∀	forall	universal quantification

This is just going through the docs quickly. There isn’t like U+XXXX RECORD MERGE so operators like & are an arbitrarily picked symbol (which is okay).

Not a solution: ligature abuse

[yannham]

Hi! This is a fair demand. I've took the liberty to turn it into an issue (#1328) which I thought more adapted to a feature request, and provides better tracking.