Zulip Chat Archive

Stream: general

Topic: simps on new style structures


Eric Rodriguez (Sep 01 2022 at 13:12):

#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 (Sep 01 2022 at 13:40):

This is for #16340, right? :)

Floris van Doorn (Sep 01 2022 at 13:47):

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 (Sep 01 2022 at 13:47):

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

Eric Rodriguez (Sep 01 2022 at 14:17):

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

Floris van Doorn (Sep 01 2022 at 15:44):

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


Last updated: Dec 20 2023 at 11:08 UTC