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

leanOutput Code action removes a ` #80

Open
nomeata opened this issue Apr 19, 2024 · 0 comments
Open

leanOutput Code action removes a ` #80

nomeata opened this issue Apr 19, 2024 · 0 comments

Comments

@nomeata
Copy link

nomeata commented Apr 19, 2024

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?

This is verso 93f84d7

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

1 participant