Does cslib have nonstandard settings?

Stream: CSLib

[Ching-Tsun Chou]

While working on a branch in cslib:
https://github.com/ctchou/cslib/commits/nat-segment/
I got two kinds of warnings that I had never seen when working on my own automata theory project, whose only dependency is mathlib. One type of warnings is this:
#new members > What does this warning mean?
The other is that when I don't want to deal with decidability issues, I used to just put open Classical at the beginning of a file. But now when I do that while working in cslib, I got the following warning:

please avoid 'open (scoped) Classical' statements: this can hide theorem statements which would be better stated with explicit decidability statements.
Instead, use open Classical in for definitions or instances, the classical tactic for proofs.
For theorem statements, either add missing decidability assumptions or use open Classical in.
Note: This linter can be disabled with set_option linter.style.openClassical false

Is there a setting specific to cslib that triggered this?

[Chris Henson]

We include in our lakefile (and check in CI) linter.mathlibStandardSet, which includes this linter.

[Ching-Tsun Chou]

I see. I just want to use classical logic and not think about "decidability" issues at all. What is the correct way to express my intent? Now I precede each offending definition or theorem with open Classical in. Is there a way for me to say: "I just want to use classical logic in this whole file"?

[Chris Henson]

I think it's not recommended to do so? The definitions need open Classical, but for the theorems you should be able to write it differently. It looks like you just want to decide if something is in a range, right? So I think you could have a local classical instance and be fine. I can look in the morning.

[Ching-Tsun Chou]

Thanks in advance! I'd appreciate any suggestions. The relevant code is in the last 2 commits of:
https://github.com/ctchou/cslib/commits/nat-segment/

[Eric Wieser]

open Classical in is indeed better practice

[Eric Wieser]

In fact, in general it's best to write

noncomputable def Nat.segment' (φ : ℕ → ℕ) (k : ℕ) : ℕ :=
  open scoped Classical in
  if k ∈ range φ then Nat.count (· ∈ range φ) k else Nat.count (· ∈ range φ) k - 1

to make clear that the scope is used only for the implementation not the signature

[Eric Wieser]

Though isn't this just Nat.count (· ∈ range φ) (k + 1) - 1?

[Ching-Tsun Chou]

Alas, you are right. I even proved a version of this myself. I'll switch to this better definition (which, to be sure, still needs open scoped Classical in).