Open
Description
From elpi Require Import elpi.
From elpi Require Import tc.
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: elpi TC.Solver.
(* Here there should be no goal left *)
Qed.What happens: we receive the list of goals: A X and B X.
Expected : Solving A X fails due to modes. B X succeeds with b setting X to nat. A nat is resumed for resolution
Actual behaviour: A X fails due to modes. B X succeeds with b setting X to nat. A nat is not resumed but returned as new goal.
Metadata
Metadata
Assignees
Labels
No labels