Lean ⟨...⟩ unfolds plain defs (whnf default); only irreducible defs block it

The anonymous constructor runs whnf on the expected type at default transparency (elabAnonymousCtor in Lean/Elab/BuiltinNotation.lean, v4.35.0), so it is not limited to reducible definitions. On Lean v4.35.0 and v4.36.0-rc2 with Mathlib, def D1 (n : ℕ) : Prop := ∃ k, k = n followed by example : D1 3 := ⟨3, rfl⟩ compiles. So do a function-valued def D4 : ℕ → Prop := fun n => ∃ k, k = n and a nested def D5 (n : ℕ) : Prop := D1 n ∧ D1 n with ⟨⟨3, rfl⟩, ⟨3, rfl⟩⟩, and so does a def-valued Mathlib ObjectProperty. It does stop at @[irreducible] def and irreducible_def, with "Invalid ⟨...⟩ notation: The expected type D2 3 is not an inductive type". obtain ⟨k, hk⟩ := h fails on the @[irreducible] one as well ("is not an inductive datatype"). Fix: unfold D2 or rw [D3_def] first. So if a ⟨...⟩ on a plain def fails with some other error (e.g. 'don't know how to synthesize implicit argument p'), reducibility is not the cause.