simps question

Stream: mathlib4

[Scott Morrison]

@Floris van Doorn:

import Mathlib.Tactic.Simps.Basic

structure P where
  x : Nat

def P.y (p : P) : Nat := p.x + 1

@[simps]
def p : P where
  x := 37

-- Is there a way to ask `simps` to generate `p_y`?
@[simp] theorem p_y : p.y = 37 + 1 := rfl

[Floris van Doorn]

No, currently that is not supported, unless P.y is definitionally equal to one of the projections.