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

Unexpected token mutual after docstring comment #4156

Closed
3 tasks done
ionathanch opened this issue May 13, 2024 · 2 comments
Closed
3 tasks done

Unexpected token mutual after docstring comment #4156

ionathanch opened this issue May 13, 2024 · 2 comments
Labels
bug Something isn't working

Comments

@ionathanch
Copy link

Prerequisites

Please put an X between the brackets as you perform the following steps:

Description

A comment block followed by a mutual block doesn't type check, possibly doesn't parse at all either

Steps to Reproduce

/-- T --/

mutual
inductive T where
end

Expected behavior: Code successfully type checks

Actual behavior: Errors with the following message:

unexpected token 'mutual'; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'simproc', 'simproc_decl', 'structure', 'syntax', 'theorem' or 'unif_hint'

Versions

4.8.0-rc1, as well as Lean nightly at https://live.lean-lang.org/#project=lean-nightly

@ionathanch ionathanch added the bug Something isn't working label May 13, 2024
@nomeata
Copy link
Contributor

nomeata commented May 13, 2024

Note that you wrote not a normal comment /- but a docstring /--, and docstrings only make sense preceding a declaration. This is probably good, but the error message could be better!

@nomeata nomeata changed the title Unexpected token mutual after block comment Unexpected token mutual after docstring comment May 13, 2024
@Kha
Copy link
Member

Kha commented Aug 22, 2024

Closing in favor of #3135

@Kha Kha closed this as not planned Won't fix, can't repro, duplicate, stale Aug 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

3 participants