(no title)
mullr | 4 years ago
Regardless, you're probably doing yourself a disservice if you're allowing things like that to take choices out of your toolbelt. Perhaps the worst offender is TLA+, where you have to write actual ascii art and latex inside your code (yes, I know model/spec). I despise it, to be clear, but it's still a pretty good tool and often the right thing to reach for
exdsq|4 years ago
Less than or equal ends up looking like:
data _≤_ : ℕ → ℕ → Set where
mullr|4 years ago