structureExt — Mathlib

Lean4
/-- The `Simps.structureExt` environment extension specifies the preferred projections of the given
structure, used by the `@[simps]` attribute.
- You can generate this with the command `initialize_simps_projections`.
- If not generated, the `@[simps]` attribute will generate this automatically.
- To change the default value, see Note [custom simps projection].
- The first argument is the list of names of the universe variables used in the structure
- The second argument is an array that consists of the projection data for each projection.
-/
@[init initFn✝, ]
opaque structureExt : NameMapExtension (List Name × Array ProjectionData)
Похожие утверждения