conv congr implication

Stream: lean4

[James Gallicchio]

Is this supposed to work in lean4 conv?

example (h : p = q) : (p → r) = (q → r) := by
  conv =>
    lhs
    congr /- invalid 'congr' conv tactic, application or implication expected
               p → r -/
    rw [h]
  sorry

The error is confusing, given that the conv target is in fact an implication.

[Reid Barton]

I don't know what this is about but it does work if p q r : Prop, so that it is really an "implication".

[James Gallicchio]

oh, this isn't even true if they're not in Prop! you're totally right. I was trying to MWE a larger error, but this is clearly not demonstrating the error, heh

[James Gallicchio]

example : True → True → True := by
  conv =>
    intro
    congr -- 'apply implies_congr' unexpected result

Okay, different but still cryptic error message :) perhaps I should be testing this in Lean3 to see if it's a regression or just a bad error message

[Mario Carneiro]

James Gallicchio said:

oh, this isn't even true if they're not in Prop!

No, it is true