Hi all. May I ask why is induction principle, say list_rect, cannot be added to any Hint database?
I tried adding it but the error: “list_rect cannot be used as a hint.” appeared.
As the documentation states: “The head symbol of the type of list_rect is a bound variable such that this tactic cannot be associated to a constant.”
More precisely, hints use the head symbol of the consequent (e.g., eq, lt) to guess when they can be used. Since list_rect has type forall P, ... -> P ..., its head symbol P is not known until the lemma has been applied.
1 Like
Thank you for your prompt reply. 