The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/09/2016 10:37 PM, Jonathan Leivent wrote:
> ...
> I think the length of the list could be eliminated by having a 
> dedicated first (or highest cost) instance of A that the second hint 
> uses to know to stop looking for more.

Like So:

Axiom A : Type.
Existing Class A.
Axiom stop : A.
Existing Instance stop | 999.
Axioms a a' b b' c c' d d' e e': A.

Class MultiA (z : list A) {x : A} := dummy : list A.

Hint Extern 0 (@MultiA ?z ?x) =>
match z with
| context [x] => fail 1
| _ => let i := eval cbv beta in(_ : @MultiA (cons x z) _) in exact i
end : typeclass_instances.

Hint Extern 0 (@MultiA ?z stop) => exact z : typeclass_instances.

Goal True.
  pose (_ : MultiA nil).


-- Jonathan