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
Signature pretty printer #375
Comments
This is even more important after #941. Instead of
we really should be printing
|
@Kha I would be interested in giving this a try. As discussed on Zulip, it seems relatively reasonable for my first issue. I'll start looking into it but I'll take any advice on where to start looking, the relevant modules and types etc. |
@Vtec234 We probably want to make sure that the output is still usable as an interactive message for widgets, correct? That is, even if the LSP hover is currently non-interactive, if we use the signature pretty printer in e.g.
Additional parameters would introduce additional contexts. |
That would be one way to do it, but maybe we just want to change the delaborator, perhaps adding a config option to select the current/new behaviour? As long as |
A signature is not a valid term syntax, so this can't be part of the delaborator unconditionally. In theory, we could introduce a purely internal delaborator option for formatting a function type as a signature suffix and then apply that option to the root when build a signature message. But I don't think we can currently embed |
OTOH, I'm not even sure we want to use the signature printer on |
But it can be valid syntax in another (adhoc) category. This is certainly not the only case where we want to embed non-term syntax in messages but which should still be interactive. E.g. tactics, commands, etc. We need to add an extra constructor for |
It's been a while since I looked at this so maybe I am missing something, but it isn't clear to me why we'd want this in the current setup, or the theoretical one in which the delaborator is changed. |
I think I misunderstood you then. Apparently you're proposing a
Not necessarily unification. The separate expression constructor is still useful for performance reasons since it delays delaboration and formatting until display time. But it would be a useful addition to store the
You can embed them into expressions using the |
@gebner So if I understood you correctly, you're not necessarily talking about extending the current delaborator (which, as a transformation from
We could add an explicit constructor for laziness. But it looks like this would not let us get rid of |
Yes, that was my proposal. Ideally the type would be
Wojciech just brought up exactly the same suggestion of adding a lazy constructor. This lazy constructor could have a hasSyntheticSorry field.
I think |
…r#375) In mathlib3, [`function.injective`](https://github.com/leanprover-community/lean/blob/4b58f26becf336a50cf037c3e2894b6f2938956e/library/init/function.lean#L73) is not reducible, so `Function.injective` should not be reducible here either. To avoid errors in `Order/Basic` ("@[ext] attribute only applies to structures or lemmas proving x = y"), we need to adjust `extAttribute` too. Fixes some problems seen in leanprover#372.
In hover text etc., we should not naively print the signature as a term to the right of the colon
:
but move parameters to the left of it, ensuring that parameter names are printed and that we can use special syntax for opt/autoParams.The text was updated successfully, but these errors were encountered: