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
While writing a blog post I was regularly confused by strange syntax errors (missing end of file), and multiple times it turned out I had
```leanOutput foo some outupt ``
in my file. Must have somehow deleted the `.
`
But right now I noticed that it was the code action that swallowed one of the `: When I have
```leanOutput evenInduct ```
and I run the code action it turns into
```leanOutput evenInduct even.mutual_induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case3 : ∀ (n : Nat), motive1 n → motive2 n) : (∀ (n : Nat), motive1 n) ∧ ∀ (n : Nat), motive2 n ``
It does only seem to happen if the code block was empty to begin with.
Maybe an off-by-one-error somewhere, or removal of what was hoped to be a \n?
\n
This is verso 93f84d7
The text was updated successfully, but these errors were encountered:
No branches or pull requests
While writing a blog post I was regularly confused by strange syntax errors (missing end of file), and multiple times it turned out I had
in my file. Must have somehow deleted the
`
.But right now I noticed that it was the code action that swallowed one of the
`
: When I haveand I run the code action it turns into
It does only seem to happen if the code block was empty to begin with.
Maybe an off-by-one-error somewhere, or removal of what was hoped to be a
\n
?This is verso 93f84d7
The text was updated successfully, but these errors were encountered: