Lean4 has truly opaque constants (constant), regular definitions (akin to Lean3's semireducible) and reducible definitions (abbrev or @[reducible]). It also does not support toggling these attributes after-the-fact. In contrast, Lean3 has irreducible as well, and allows arbitrary switching among reducibility types. The current mismatch is a source of major performance problems in auto-ported Mathlib, e.g. when the elaborator tries to unfold real.pi. The tentative consensus from previous discussions was that these changes should be back-ported to Mathlib (even if not enforced by Lean3 itself).
Lean4 has truly opaque constants (
constant), regular definitions (akin to Lean3'ssemireducible) and reducible definitions (abbrevor@[reducible]). It also does not support toggling these attributes after-the-fact. In contrast, Lean3 hasirreducibleas well, and allows arbitrary switching among reducibility types. The current mismatch is a source of major performance problems in auto-ported Mathlib, e.g. when the elaborator tries to unfoldreal.pi. The tentative consensus from previous discussions was that these changes should be back-ported to Mathlib (even if not enforced by Lean3 itself).