search

FissoreD / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
0 stars 0 forks source link

Typeclasses eauto does not call elpi's solver #16

Open FissoreD opened 3 weeks ago

FissoreD commented 3 weeks ago 
From elpi Require Import tc.
From elpi Require Import elpi.

  TC.Pending_mode !.
  Class A (i: Type).
  Global Hint Mode A ! : typeclass_instances.

  Class B (i :Type).

  Instance a: A nat := {}.
  Instance b: B nat := {}.

  Goal exists X, A X /\ B X.
    eexists; split.
    all: typeclasses eauto. (* Typeclasses eauto does not call TC.Solver *)
  Abort.