Stream: math-comp users

Topic: have an typeclasses


view this post on Zulip Matthieu Sozeau (May 17 2021 at 13:10):

Is there anything against having a flag for have so that have foo := bar allow typeclass resolution in bar to happen? I often want to assert a sublemma giving enought arguments for its tc premises to be resolved, and right now I must use set and clearbody to emulate the have I want

view this post on Zulip Kazuhiko Sakaguchi (May 17 2021 at 19:46):

@Matthieu Sozeau If you do not change the behavior of have, I think this is the workaround you need: https://github.com/math-comp/analysis/blob/8a8036faa787171d9c4773934fc2b9d1d5cf3b13/theories/posnum.v#L45-L46

view this post on Zulip Matthieu Sozeau (May 17 2021 at 21:35):

I see, thanks!


Last updated: Mar 28 2024 at 19:02 UTC