Zulip Chat Archive
Stream: lean4
Topic: Warning when I use a constant function
Kind Bubble (Dec 02 2022 at 00:12):
Whenever I make use of a constant function I get this warning:
Main.lean:524:238: warning: unused variable ‘q‘ [linter.unusedVariables]
I was wondering how I could turn this off, or maybe someone knows a way to produce a constant function which is a recommended alternative.
Kevin Buzzard (Dec 02 2022 at 00:19):
Just replace q with _
Last updated: Dec 20 2023 at 11:08 UTC