eq.subst for Type

Stream: general

[Yaël Dillies]

Why is docs#eq.subst only for Prop?

[Eric Wieser]

docs#eq.rec

[Eric Wieser]

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

[Eric Wieser]

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

[Kyle Miller]

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]

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]

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

[Eric Rodriguez]

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