Or Agda where you basically have to use emacs with the agda extension to get all the characters.

Less than or equal ends up looking like:

data _≤_ : ℕ → ℕ → Set where

   z≤n : {n : ℕ} → zero ≤ n

   s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m