Marcus Rossel

@robertylewis Yes, the description is outdated. We use Lean and Coq for the exercises. Unfortunately the lecture slides and exercises are in private repositories. I'll ask the lecturer if he'd...

@sertel, could you create a new public repo from the `no-solution` branch of the `fcplcd-exercises` repo? Then I could link to the exercise sheets in this PR.

I'm confused about the very first post in this thread. In the example: ```c reaction(startup) -> a, b {= // Based on this reaction body, it looks like a and...

@semorrison I have a fix for the Mathlib breakage lying around locally. Could I please have permission to push to the corresponding Mathlib branch?

> Does it make sense to fix #2678 first before removing all such lemmas from mathlib `dsimp` calls? I think that's not necessary. Fixing Mathlib's `dsimp` calls amounted to simply...

Ah ok, then it seems I don't understand the following point yet: What's the benefit of keeping `dsimp` arguments (the `Iff.rfl` arguments) which aren't actually necessary for the proof to...

> the proofs that follow those `dsimp`s will likely end up being longer or messier than necessary as a workaround. I just compared the proofs which are affected by this...

@semorrison thanks! I'm just waiting on #2678 to be resolved before continuing with this PR. Is there some way I can indicate that this PR is waiting for another PR/issue?

@eric-wieser Ok, then the question remains how to check for `Iff`-rfl proofs. Do you think adjusting `isRflProof` as follows would be a good idea? It takes approach for checking `Iff`-rfl...

Ich weiß nicht wie es so generell laufen soll, aber ich bin der Meinung, dass Vorlesungen nicht unbedingt _exakt_ auf einander abgestimmt werden sollten. Ansonsten ist es für Einsteiger deutlich...