chore: use terminology "non-recursive structure" instead of "struct-like"

[kmill]

This PR changes "structure-like" terminology to "non-recursive structure" across internal documentation, error messages, the metaprogramming API, and the kernel, to clarify Lean's type theory. A structure is a one-constructor inductive type with no indices — these can be created by either the structure or inductive commands — and are supported by the primitive Expr.proj projections. Only non-recursive structures have an eta conversion rule. The PR description contains the APIs that were renamed.

Addresses RFC #5891, which proposed this rename. The change is motivated by the need to distinguish between structure-defined structures, structures, and non-recursive structures. Especially since #5783, which enabled the structure command to define recursive structures, "structure-like" has been easy to misunderstand.

Changes:

• Kernel: is_structure_like() -> is_non_rec_structure()
• Lean.isStructureLike -> Lean.isNonRecStructure
• Lean.matchConstStructLike -> Lean.matchConstNonRecStructure
• Lean.getStructureLikeCtor? -> Lean.getNonRecStructureCtor?
• Lean.getStructureLikeNumFields -> Lean.getNonRecStructureNumFields
• Lean.Expr.proj: extended and corrected documentation (note: despite the fact that not every projection can be written as a recursor application, I left in this claim since it seems good to document a more-restrictive specification, and some users have requested the kernel be more restrictive in this way)

Closes #5891

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ec565f3bf7a3985b6b8592f5cb5fa063b86a0ecf --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-01 19:31:08)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ec565f3bf7a3985b6b8592f5cb5fa063b86a0ecf --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-03-01 19:31:09)

[Rob23oba]

Terminology question: Is Exists a non-recursive structure? At least the function says yes but Exists doesn't have an eta rule. For my project that meant adding a new function, isStructureLikeWithLargeElim, that does a better job at figuring these things out.

[kmill]

@Rob23oba Yes, Exists is a non-recursive structure. The eta rule applies for non-recursive structures, if the projections all exist, but they don't exist for Exists since it doesn't have large elimination.