ProjectionRule — Mathlib

Lean4
/-- The type of rules that specify how metadata for projections in changes.
See `initialize_simps_projections`. -/
inductive ProjectionRule where/-- A renaming rule `before→after` or
    Each name comes with the syntax used to write the rule,
    which is used to declare hover information. -/

  | rename (oldName : Name) (oldStx : Syntax) (newName : Name) (newStx : Syntax) : ProjectionRule/--
An adding rule `+fieldName` -/

  | add : Name → Syntax → ProjectionRule/-- A hiding rule `-fieldName` -/

  | erase : Name → Syntax → ProjectionRule/-- A prefix rule `prefix fieldName` -/

  | prefix : Name → Syntax → ProjectionRule
Похожие утверждения