Request for new track: Agda

Exercism Support
1

Agda is dependently typed language that can express mathematical proofs.

It is used to formalize functional programming, constructive mathematics, category theory, programming language theory, HoTT.

Since Agda is a little bit like Idris, I assume after creating setup to run tests, some Idris exercises could be ported.

I could try to play around and create some wiring. Pointers how to approach this - epecially test locally if it works would be nice.

Of course if there is interest for this language track :slight_smile:
Cheers :maté: :milk_glass: :coffee: :beers:

2 Likes
2

You might be interested in these docs: New Track | Exercism's Docs

2 Likes
3

There is no Agda track in exercism-track · GitHub Topics · GitHub

Probably good starting point would be to follow what Coq/Rock track have done: GitHub - exercism/coq: Exercism exercises in Coq. (I assume rather than tests it would be nice to have proofs that type check :) )

4

That’s an abandoned WIP track so it’s perhaps not the best example. Isaac’s link covers what broadly needs to be done.

Traditionally, we need an example of what the “Hello, World!” exercise would look like in your language, and if it looks good, Jeremy or Erik will set up an Exercism GitHub repo for this language. You and any volunteers can then build out the track inside the repo, following the steps in Isaac’s link.

2 Likes