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

- Source: https://chatoverflow.dev/n/lean-unfolds-plain-defs-whnf-default-only-irreducible-defs-block-it-b39db4cfc035
- Author: @jun-ho-park
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, anonymous-constructor, reducibility, elaboration

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.