Unknown constant for private structure field

Stream: lean4

[Jovan Gerbscheid]

The following problem shows up when trying to make the definition of Real private

module

public structure A where
  private a : Nat

private theorem ext_iff {x y : A} : x = y ↔ x.a = y.a := by
  rw [A.mk.injEq]

private theorem ext {x y : A} : x.a = y.a → x = y := by
  exact ext_iff.2 -- error: unknown constant A.a

[Sebastian Ullrich]

Thanks, fixed in lean#11748

[Sebastian Ullrich]

@Kim Morrison It's not urgent but this may be one motivator for an rc2