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

help separator is too fancy #660

Closed
brianhuffman opened this issue Nov 20, 2019 · 1 comment
Closed

help separator is too fancy #660

brianhuffman opened this issue Nov 20, 2019 · 1 comment

Comments

@brianhuffman
Copy link
Contributor

Today I wanted to check the precedence level of the == operator, and I was surprised to see this output:

Cryptol> :? ==

    primitive type (==) : # -> # -> Prop

Precedence 20, does not associate.

Assert that two numeric types are equal.

            ~~~ * ~~~

    (==) : {a} (Cmp a) => a -> a -> Bit

Precedence 20, does not associate.

Compares any two values of the same type for equality.

I was initially confused about the meaning of ~~~ * ~~~, because I was looking up information about infix operators, and ~~~ and * also look like infix operators. After a moment I realized that they were intended to be a purely decorative visual separator.

We should replace this string with something less fancy; we're not typesetting a novel here :) Considering that this separator will be seen quite infrequently (only when using :? on an identifier that has both type-level and value-level definitions with documentation) we should have something that is undistracting even for someone seeing it for the first time. Perhaps a line of hyphens?

@yav
Copy link
Member

yav commented Nov 20, 2019

Maybe we can add Chapters! I don't have a strong opinion on what we use, but I think having some separator is nice---I added the fancy line because in the previous version it was hard see where the different sections ended.

Another UI design choice I wondered about but couldn't come to a decision was if we should have a separator, or some sort of leading marker on each section. I went with the separator thinking that having multiple sections is relatively rare, so I thought maybe the extra noise of a leading marker would be distracting when there is only one section.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants