[Agda-dev] Implementing a solver for universe levels

[Jesper Cockx]

Hi Marko,

That's great to hear! Let's continue the discussion on the github page for
that issue.

-- Jesper

On Tue, Jan 7, 2020 at 8:48 PM Marko Dimjašević <marko at dimjasevic.net>
wrote:

> 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 --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20200107/c63e169e/attachment.html>