add detector from using Classical.choice

[awalterschulze]

Seems Classical.choice is used quite a bit more than I would have thought:

% lake build
⚠ [679/690] Replayed Katydid.Std.Lists
warning: ././././Katydid/Std/Lists.lean:50:4: 'Lists.mergeReps' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Std/Lists.lean:442:8: 'list_take_take' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Std/Lists.lean:653:8: 'list_take_length' depends on 'Classical.choice' on axioms: [propext, Classical.choice, Quot.sound]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Std/Lists.lean:767:8: 'list_prefix_leq_length' depends on 'Classical.choice' on axioms: [propext, Classical.choice, Quot.sound]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Std/Lists.lean:791:8: 'list_drop_app' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Std/Lists.lean:803:8: 'list_drop_app'' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Std/Lists.lean:825:8: 'list_prefix_length_leq' depends on 'Classical.choice' on axioms: [propext, Classical.choice, Quot.sound]
note: this linter can be disabled with `set_option linter.detectClassical false`
⚠ [681/690] Replayed Katydid.Std.Balistic
warning: ././././Katydid/Std/Balistic.lean:483:0: declaration uses 'sorry'
warning: ././././Katydid/Std/Balistic.lean:503:0: declaration uses 'sorry'
warning: ././././Katydid/Std/Balistic.lean:508:0: declaration uses 'sorry'
⚠ [682/690] Replayed Katydid.Std.NonEmptyList
warning: ././././Katydid/Std/NonEmptyList.lean:49:4: 'NonEmptyList.eraseReps' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Std/NonEmptyList.lean:59:4: 'NonEmptyList.mergeReps' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
⚠ [684/690] Replayed Katydid.Regex.Language
warning: ././././Katydid/Regex/Language.lean:735:8: 'Language.simp_not_not_is_double_negation' depends on 'Classical.choice' on axioms: [Quot.sound,
 propext,
 Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/Language.lean:740:8: 'Language.simp_not_and_demorgen' depends on 'Classical.choice' on axioms: [Quot.sound, propext, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
ℹ [685/690] Replayed Katydid.Regex.SimpleRegex
info: ././././Katydid/Regex/SimpleRegex.lean:275:0: 'SimpleRegex.decidableDenote' depends on axioms: [propext, Quot.sound]
⚠ [686/690] Replayed Katydid.Regex.IndexedRegex
warning: ././././Katydid/Regex/IndexedRegex.lean:46:4: declaration uses 'sorry'
warning: ././././Katydid/Regex/IndexedRegex.lean:50:4: declaration uses 'sorry'
warning: ././././Katydid/Regex/IndexedRegex.lean:50:4: declaration uses 'sorry'
warning: ././././Katydid/Regex/IndexedRegex.lean:50:4: declaration uses 'sorry'
⚠ [687/690] Replayed Katydid.Regex.SmartRegex
warning: ././././Katydid/Regex/SmartRegex.lean:316:4: 'SmartRegex.orFromList' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:343:8: 'SmartRegex.orToList_is_orFromList' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:388:4: 'SmartRegex.smartOr' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:426:16: declaration uses 'sorry'
warning: ././././Katydid/Regex/SmartRegex.lean:443:8: declaration uses 'sorry'
warning: ././././Katydid/Regex/SmartRegex.lean:443:8: 'SmartRegex.smartOr_is_or' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice, sorryAx]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:505:4: 'SmartRegex.derive' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:519:8: 'SmartRegex.derive_commutes' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice, sorryAx]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:610:4: 'SmartRegex.derives' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:614:8: 'SmartRegex.derives_commutes' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice, sorryAx]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:632:4: 'SmartRegex.validate' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:636:8: 'SmartRegex.validate_commutes' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice, sorryAx]
note: this linter can be disabled with `set_option linter.detectClassical false`
warning: ././././Katydid/Regex/SmartRegex.lean:645:4: 'SmartRegex.decidableDenote' depends on 'Classical.choice' on axioms: [propext, Quot.sound, Classical.choice, sorryAx]
note: this linter can be disabled with `set_option linter.detectClassical false`
⚠ [688/690] Replayed Katydid.Expr.Desc
warning: ././././Katydid/Expr/Desc.lean:154:4: declaration uses 'sorry'
warning: ././././Katydid/Expr/Desc.lean:166:4: declaration uses 'sorry'
warning: ././././Katydid/Expr/Desc.lean:178:4: declaration uses 'sorry'
warning: ././././Katydid/Expr/Desc.lean:227:8: declaration uses 'sorry'
Build completed successfully.

Good detections include:
Language.simp_not_not_is_double_negation

Some surprises of using Classical.choice include:

def orFromList (xs: NonEmptyList (Regex α)): Regex α :=
  match xs with
  | NonEmptyList.mk x1 [] =>
    x1
  | NonEmptyList.mk x1 (x2::xs) =>
    Regex.or x1 (orFromList (NonEmptyList.mk x2 xs))

where NonEmptyList is defined as:

structure NonEmptyList (α: Type) where
  head : α
  tail : List α

So I am not sure how avoidable this is in the general in Lean