3 ms·
Check out Lean Prover's online editor: https://leanprover.github.io/live/latest/ https://leanprover.github.io/live/latest/ They borrow syntax from LaTeX math-m
by codebje 7y ago
Check out Lean Prover's online editor: https://leanprover.github.io/live/latest/ https://leanprover.github.io/live/latest/
They borrow syntax from LaTeX math-mode to allow symbol entry, such that you can type "\ne" and as soon as you hit the space after the "e", you get ≠ instead.
The language plugin for Visual Studio Code does the same thing.
Lean Prover's not exactly a programming language, but :
def foo (a b : ℕ) : ℕ → ℕ → ℕ :=
λ a b, a + b
Still looks decent.
I think it has to be all or nothing though, since if it's optional the odds of getting decent editor support for it is low.