-
Notifications
You must be signed in to change notification settings - Fork 80
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
Annotate pretty-printed output with full constant names #89
Conversation
This allows the debug build to build mathlib.
I also added a |
Do you think with the full knowledge of type information, we could link to the correct instance of a typeclass rather than the typeclass itself? E.g. the |
I would also like to see that. In practice I'm not sure there's an always an obvious choice for the instance declaration. E.g. in your example with |
This looks good to me. I especially like what you did to pretty print projections. Ready to merge? |
Yes, I think this can be merged. The |
08a832d
to
217862b
Compare
For doc gen reasons, could I request that this PR be included in a 3.5 release before we officially move mathlib over to 3.5? |
Certainly. Sorry I completely lost sight of this PR. We can schedule 3.5.1 in the near future to make this PR available. Let's see if you have backward compatible PRs until then. |
@cipher1024 In advance of the shift to 3.5c, could we merge this so it's part of the nightlies? |
This uses `U+E003` (the next available private use character after the ones claimed in #89) to prefix the names: * `pi` * `forall` * `function` * `implies` * `Sort` * `Prop` * `Type` The motivation is to be able to link these ideas in doc-gen.
Motivation: we want to have links for all constants in the API documentation, even if they are behind notation. See companion PR leanprover-community/doc-gen#3.
This PR adds the option
pp.links
which, if set to true, annotates things likeℤ
and+
and thefst
inp.fst
with the corresponding constant names (i.e.,int
,has_add.add
, andprod.fst
). The markup syntax for this annotation is as follows:<U+E000>prod.fst<U+E001>fst<U+E002>
The Unicode code points
U+E000
,U+E001
,U+E002
are taken from the Private Use Area. Hopefully nobody uses them for anything else.