Felix Cherubini

Yes, that is what I understand as well. The problem I suspected, is with the variable 'ring'. It should be outside the pi when we start and under the lambdas...

I finally wrote down some tests/examples. As it turns out, integers seem not to normalize correctly (don't understand why). This is the first example (-module) here: ``` https://github.com/felixwellen/agda-stdlib/blob/issue-1116-generic-ring-solve/src/Tactic/RingSolver/Examples.agda ``` And...

> How about including our Github handles together with our names? Yes - but I would turn the list into a table then...

I like it - what do you think: https://github.com/felixwellen/cubical/tree/885_update_readme#reviewing-of-pull-requests

I sorted stuff in the README by topic and threw in some headlines. Someone with knowledge of this stuff should look at it: @mortberg

> @ecavallo What do you want listed as your area of expertise? Most things? I guess you mean the same as you area of expertise, which is "Most topics"?

Putting this back to 'draft' - maybe it is better, if we actually use the 'Assign' field of the PRs. That way it is much easier, to get an overview...

There was one open question: Should we make use of assigning PRs? But I'll write an issue for that and we discuss it on the next meeting. So, yes, ready...

Done: #905

We have the bullet point in CONTRIBUTING.md. So it remains to be checked, if there are still public imports that should not be public.