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
@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
I see, thanks!
Last updated: Mar 28 2024 at 19:02 UTC