Skip to content

Add missing "set_option linter.unusedVariables false"#174

Open
ozgurakgun wants to merge 2 commits into
leanprover:masterfrom
ozgurakgun:patch-2
Open

Add missing "set_option linter.unusedVariables false"#174
ozgurakgun wants to merge 2 commits into
leanprover:masterfrom
ozgurakgun:patch-2

Conversation

@ozgurakgun

Copy link
Copy Markdown

without this hq is marked with the "unused variable hq" warning.

without this `hq` is marked with the "unused variable `hq`" warning.
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

Successfully merging this pull request may close these issues.

1 participant