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

Elim on a variable already in the context? #156

Open
favonia opened this issue Jun 9, 2020 · 1 comment
Open

Elim on a variable already in the context? #156

favonia opened this issue Jun 9, 2020 · 1 comment
Labels
blocked

Comments

@favonia
Copy link
Collaborator

favonia commented Jun 9, 2020

@jonsterling
@jonsterling
Copy link
Collaborator

My first thought is to not support this directly until we have some sick tactics that can generalize the goal properly --- it is not enough to generalize the goal using generalize, since we need to reformulate the generalized goal into a Kan type code. All this is possible, but it's currently a little tricky.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
blocked
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@jonsterling @favonia