I’m trying to have a succinct notation for defining instances using a tactic. However, it seems that defining instances this way may cause a significant slowdown. I’m afraid a self-contained example will be hard to extract, but my situation is similar to the following:
Class C (arg : Prop) := class_def : arg -> arg. (* some complicated prop dependent on arg *) Ltac solve := unfold C; intros a; exact a. (* some expensive tactic *) Instance holds1 : C True := ltac:(solve). (* takes 3 minutes for the actual instance *) Definition holds2 : C True := ltac:(solve). (* takes 25 seconds .. *) Instance holds3 : C True. Proof. solve. Defined. (* takes 25 seconds .. *) Instance holds4 : C True. Proof. solve. Qed. (* takes 25 seconds .. *)
Does anyone have an idea what might cause this? I would expect that at least
holds2 take the same amount of time.