4 ms·

I program in Agda pretty often and community usually uses Unicode characters for most things, so I do too. The impl of AVL trees in stdlib: https://github.com/

I program in Agda pretty often and community usually uses Unicode characters for most things, so I do too. The impl of AVL trees in stdlib: https://github.com/agda/agda-stdlib/blob/master/src/Data/Tree/AVL.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Tre... Some basic properties of natural numbers: https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Properties.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat... It makes the code look absolutely gorgeous, readable and it's very easy to type too. I use Emacs agda-mode so it just automatically replaces e.g. \r with → or \== with ≡ etc... I don't use Agda for theorem proving, I make real life programs in Agda, I compile them to Haskell and compile with GHC to executables.

fwip 6y ago
That's pretty cool. What kind of problems do you find yourself solving with your Agda code? (Or, asked another way, what sort of stuff do your programs do?)
- gnulinux 6y ago
  Currently my programs parse text. I have a JSON formatter, a lisp formatter. I'm also writing an Agda preprocessor in Agda i.e. parse Agda-like code, process it, print valid Agda code. I use them in my other projects as tooling. Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.
ColanR 6y ago
What font do you use for this? It looks weird with my defaults. I once seriously considered trying to build something that included math symbols in the syntax. It's pretty cool to see that I don't have to.
- gnulinux 6y ago
  Not currently on my computer with that setup but afair I use Inconsolata.
arthurcolle 6y ago
Julia also allows Unicode characters, which I think is great for math-heavy programs. I love that about it. I always forget the keybindings for them though.
- gnulinux 6y ago
  agda-mode in emacs has fallback option for latex like aliases. E.g. \infty gives ∞ or \cdot gives · it's very convenient if you use latex often. Other than that, if you have no clue, M-x describe-char explains you how to produce a character.
Camillo 6y ago
> I use Emacs agda-mode I think Emacs is basically required to use Agda, right? To the point that the set of Agda users is a strict subset of the set of Emacs users.
- gnulinux 6y ago
  Pretty much, yes. It's not "required" required, but in order to use the stdlibrary (i.e. use Unicode chars) you need to use Emacs and Emacs mode is extremely useful to develop Agda code. You can still compile and type check using `agda` binary but that's pretty much the only thing you can do.

fwip 6y ago

That's pretty cool. What kind of problems do you find yourself solving with your Agda code? (Or, asked another way, what sort of stuff do your programs do?)

gnulinux 6y ago
Currently my programs parse text. I have a JSON formatter, a lisp formatter. I'm also writing an Agda preprocessor in Agda i.e. parse Agda-like code, process it, print valid Agda code. I use them in my other projects as tooling. Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.

ColanR 6y ago

What font do you use for this? It looks weird with my defaults. I once seriously considered trying to build something that included math symbols in the syntax. It's pretty cool to see that I don't have to.

gnulinux 6y ago
Not currently on my computer with that setup but afair I use Inconsolata.

arthurcolle 6y ago

Julia also allows Unicode characters, which I think is great for math-heavy programs. I love that about it. I always forget the keybindings for them though.

gnulinux 6y ago
agda-mode in emacs has fallback option for latex like aliases. E.g. \infty gives ∞ or \cdot gives · it's very convenient if you use latex often. Other than that, if you have no clue, M-x describe-char explains you how to produce a character.

Camillo 6y ago

> I use Emacs agda-mode I think Emacs is basically required to use Agda, right? To the point that the set of Agda users is a strict subset of the set of Emacs users.

gnulinux 6y ago
Pretty much, yes. It's not "required" required, but in order to use the stdlibrary (i.e. use Unicode chars) you need to use Emacs and Emacs mode is extremely useful to develop Agda code. You can still compile and type check using `agda` binary but that's pretty much the only thing you can do.