Zulip Chat Archive

Stream: general

Topic: eq.subst for Type

Yaël Dillies (Oct 14 2021 at 21:15):

Why is docs#eq.subst only for Prop?

Eric Wieser (Oct 14 2021 at 21:53):


Eric Wieser (Oct 14 2021 at 21:54):

See also docs#cast, docs#eq.mp, docs#eq.mpr

Eric Wieser (Oct 14 2021 at 21:54):

I suspect eq.subst exists because of its mysterious subst attribute (docs#eq.subst)

Kyle Miller (Oct 15 2021 at 07:07):

What does the subst attribute do?

(Another somewhat mysterious attribute is congr. When updating the simp documentation I ran into it, and I have some idea of what it does, but it shows up in some surprising places.)

Eric Rodriguez (Oct 15 2021 at 07:43):

I think some attributes are historical artifacts that never got turned into features. The one I really wish was a thing was the one on funext, which is intro! . I really like the idea of combining intro and ext

Reid Barton (Oct 15 2021 at 11:39):

Doesn't ext do that? Or do you mean combining them another way?

Eric Rodriguez (Oct 15 2021 at 12:03):

I mean yes, I just wish I didn't have to write intro...,ext..., or even with some hyperadvanced lambda we could just do \lam [...], by simpinstead of the standard ext;simp

Last updated: Aug 03 2023 at 10:10 UTC