I have an instance of a typeclass
C where one instance looks like
S -> C x f1 -> C y f2 -> C (x * y) f3 (here
S is a side-condition, typically
x <> 0). Even if
S is one of the assumption of my goal, the instance fails to be applied by resolution. What is the standard way to deal with this kind of situation?
I don't know if it is usual, but you could declare the instance using the Hint Extern machinery on the TC instance database, apply you instance by hand (with
apply) and call, say,
assumption on the first goal.
thanks, is there an example somewhere of this kind of use of
Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
I think assumptions were always used, even for non-typeclasses, so this might be a different bug, such as simple apply being too weak?
maybe the context item is not syntactically identical to the goal (typical situation in mathcompland)
Enrico may be right, when tracing the resolution I see the step of my side condition but at the end it says
did you manage to call
assumption in the hint extern?
Last updated: Jan 29 2023 at 05:03 UTC