search

FissoreD / coq-elpi

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

Mode + Link activation (HO variable) #11

Open FissoreD opened 1 month ago

FissoreD commented 1 month ago

Here the premise force-llam-t is not compiled

TC.Pending_mode !.
Class A (i: Type).
Global Hint Mode A ! : typeclass_instances. (*Mode also added in elpi*)

Axiom f : Type -> Type.
Axiom g : Type -> Type.

Class B (i :Type).

Instance i: forall X (Y: Type), (forall x, A (X x)) -> B (X Y) := {}.

Instance a x : A (f x) -> A (f x) := {}.

Elpi Print TC.Solver.

Goal B (g nat).
  (* Elpi Override TC TC.Solver None. *)
  (* Set Elpi Typeclasses Debug. *)
  Timeout 1 apply _. (* -> Here the premise (forall x, A (X x)) is called with a flexible X *)
Qed.