We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
Consider this example. The notation for three is not pretty-printed.
three
def two := 2 notation "𝟚" => two /- 𝟚 : Nat -/ #check 𝟚 def three (_ : Nat) := 3 notation "𝟛" => three /- three 10 : Nat -/ #check 𝟛 10
Expected behavior: We see 𝟛 10 : Nat in the message.
𝟛 10 : Nat
Actual behavior: We see three 10 : Nat.
three 10 : Nat
Reproduces how often: 100%
nightly-2022-07-22
The text was updated successfully, but these errors were encountered:
Successfully merging a pull request may close this issue.
Description
Consider this example. The notation for
three
is not pretty-printed.Steps to Reproduce
Expected behavior: We see
𝟛 10 : Nat
in the message.Actual behavior: We see
three 10 : Nat
.Reproduces how often: 100%
Versions
nightly-2022-07-22
The text was updated successfully, but these errors were encountered: