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.

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

Show the result of a meta definition #113

Closed
valis opened this issue Feb 21, 2020 · 6 comments · Fixed by #156
Closed

Show the result of a meta definition #113

valis opened this issue Feb 21, 2020 · 6 comments · Fixed by #156
Assignees
@ice1000
Labels
feature meta subexpr
Milestone
1.3

Comments

@valis
Copy link
Collaborator

@valis valis commented Feb 21, 2020

Implement an action that show the result of the meta definition under the cursor.
@valis valis added this to the 1.3 milestone Feb 21, 2020
@ice1000
Copy link
Collaborator

@ice1000 ice1000 commented Mar 6, 2020

Already implemented in some sense:
image

@valis
Copy link
Collaborator Author

@valis valis commented Mar 6, 2020

"Meta definitions" are tactics, not "meta variables"

@ice1000
Copy link
Collaborator

@ice1000 ice1000 commented Mar 6, 2020

Oh

@ice1000
Copy link
Collaborator

@ice1000 ice1000 commented Mar 6, 2020

image
How 'bout this?

@ice1000
Copy link
Collaborator

@ice1000 ice1000 commented Mar 6, 2020

However, normalizing it to WHNF doesn't show a well-typed expr:

image

@valis
Copy link
Collaborator Author

@valis valis commented Mar 6, 2020

It would be convenient to show the non-normalized result.

It does not type-check because it doesn't print implicit arguments for Equiv.

@valis valis added the meta label Mar 8, 2020
@ice1000 ice1000 mentioned this issue Mar 10, 2020
Merged
@ice1000 ice1000 self-assigned this Mar 11, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ice1000 ice1000

Labels
feature meta subexpr
Projects
None yet
Milestone
1.3
Development

Successfully merging a pull request may close this issue.

Implement 154 JetBrains/intellij-arend
2 participants
@valis @ice1000