The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jason,

Michael, your tactic fails in the case where there are ambiguous instances.  There is a way around this: you can construct a typeclass that takes in a list and another class and is resolved by an instance of that class not in the list.  By applying this recursively, you can get the first n instances of any class.

You are right. I think there might be a simpler way, though: use eauto to construct something which consists out of the typeclass instance and the equality. Then this can be solved with eauto backtracking.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928