simps on new style structures

Stream: general

[Eric Rodriguez]

#mwe:

import algebra.order.field

structure my_class extends ℕ →+ ℕ :=
(w : to_fun 37 = 0)

instance : has_coe_to_fun (my_class) (λ f, ℕ → ℕ) := ⟨λ f, f.to_fun⟩

initialize_simps_projections? my_class

set_option old_structure_cmd true

structure my_class' extends ℕ →+ ℕ :=
(w : to_fun 37 = 0)

instance : has_coe_to_fun (my_class') (λ f, ℕ → ℕ) := ⟨λ f, f.to_fun⟩

initialize_simps_projections? my_class'

I can't seem to get the coe projections to work properly on new-style structures. Note that my_class' uses the coe projection, whilst my_class doesn't. How can I fix this?

[Anne Baanen]

This is for #16340, right? :)

[Floris van Doorn]

Search the library for "We need to specify this projection explicitly in this case" and mimic what is done in all those cases.

[Floris van Doorn]

you need to define a my_class.simps.apply function manually with the projection you want simps to use.

[Eric Rodriguez]

ahh, I see that what Anne suggested is a common workaround :) should I draft a library note about this?

[Floris van Doorn]

What's wrong with the library note that Anne linked?