Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

"Dependent induction is not allowed for inductive definition" should describe why dependent induction is not allowed #20032

Open
JasonGross opened this issue Jan 12, 2025 · 2 comments
Open

"Dependent induction is not allowed for inductive definition" should describe why dependent induction is not allowed #20032

JasonGross opened this issue Jan 12, 2025 · 2 comments
Labels
kind: user messages Error messages, warnings, etc. kind: wish Feature or enhancement requests.

Comments

@JasonGross
Copy link
Member

Is your feature request related to a problem?

I'm trying to debug SkySkimmer/coq-lean-import#21 (comment), and it's a bit hard without having more information.

Proposed solution

At least I'd like (the option) to have it print the inductive declaration and not just its name. More fine-grained information would probably be better.

Alternative solutions

No response

Additional context

No response
@JasonGross JasonGross added needs: triage The validity of this issue needs to be checked, or the issue itself updated. kind: wish Feature or enhancement requests. labels Jan 12, 2025
@SkySkimmer
Copy link
Contributor

At least I'd like (the option) to have it print the inductive declaration and not just its name.

Why though?

@SkySkimmer SkySkimmer added kind: user messages Error messages, warnings, etc. and removed needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Jan 12, 2025
@JasonGross
Copy link
Member Author

Ah, I thought the justification had something to do with the type of constructors / the inductive family. If the restriction is just about what options are set, then I think an explanation like "Dependent induction is not allowed for inductive definition $name because it has primitive projections but not eta" or w/e is sufficient.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: user messages Error messages, warnings, etc. kind: wish Feature or enhancement requests.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JasonGross @SkySkimmer