3 ms·
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 _≤_ : ℕ → ℕ → S
by exdsq 5y ago
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
- mullr 5y agoAnd to really rub salt on it, they have a syntax that looks very much like stock latex for math symbols, and SOME of them are the same, but not all of them! (all / forall is the one that comes to mind, it's been a little while)
- hwayne 5y agoIt always ALWAYS trips me up that TLA+ uses \A and \E while LaTeX uses \forall and \exists