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