[Agda-dev] Implementing a solver for universe levels
Marko Dimjašević
marko at dimjasevic.net
Tue Jan 7 20:47:24 CET 2020
Dear Jesper,
On Mon, 2020-01-06 at 10:26 +0100, Jesper Cockx wrote:
> Since you're a new contributor to Agda, my recommendation would be to
> start on something smaller to get a feeling for the Agda codebase. If
> you want to do this, here are some issues related to universe levels
> that currently need help: https://github.com/agda/agda/issues/4345,
> https://github.com/agda/agda/issues/4119,
> https://github.com/agda/agda/issues/3143.
Thank you a lot for your detail reply!
I will take your suggestion and start with a smaller task. In
particular, if you are OK with it, I'd start off with
https://github.com/agda/agda/issues/4345.
I suppose these are the first and general things to understand for me:
- https://github.com/agda/agda/blob/master/HACKING.md
-
https://github.com/andreasabel/haskell-style-guide/blob/master/haskell-style.md
Do you have anything to add that is specific to issue 4345?
--
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
PGP key ID: 056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20200107/d993cca6/attachment.sig>
More information about the Agda-dev
mailing list