Mysterious error message

Stream: lean4

[Joris Roos]

(using Lean version 4.15.0-nightly-2024-11-15)

structure A where
  p: Prop
  q: True

structure B extends A where
  q': p → True

example: B where
  p := True ∧ True
  q := by exact True.intro
  q' := λ ⟨_,_⟩ ↦ True.intro

gives the unexpected kernel error (kernel) declaration has metavariables '_example'

Mysteriously (to me), any one of the following changes make the error disappear:

• replacing by exact True.intro by True.intro
• replacing ⟨_,_⟩ by _
• moving any of p, q into B (or q' into A)

Could someone shed some light on this?

[Kim Morrison]

Sorry about the slow reply on this. I wonder if this is the same issue as lean#5925.

[Kim Morrison]

If you want to open an issue, perhaps link to that one?

[Joris Roos]

Thanks, I opened a new issue: lean#6354

[Kyle Miller]

(Discussion continues here)