Lean FRO Meeting - Leonardo de Moura

Stream: Lean Together 2024

[Mario Carneiro]

@Joachim Breitner In the example which shows a matrix of decreasing / equal relations, there was an all-=example. In this specific case, it is impossible to prove decreasing, so it might make sense to skip the normal guessing process and just show a more targeted error directly on this call

[Joachim Breitner]

Right, that was suggested before, and I agree that there are plenty of special cases where the message could be made nicer. I guess someone just has to do it. I’ll open an issue and maybe I’ll do it when I have appetite for some low hanging fruit, or someone else wants to get to know the code.

https://github.com/leanprover/lean4/issues/3172

[Mario Carneiro]

Is there an issue for rw [x] and simp [x] where x is a let variable?

[Matthew Ballard]

Here is the issue re:noncomputable section lean4#2619.

What I heard from the discussion was the proposal to change the semantics of noncomputable section to that of suppress_compilation.