_aux_Mathlib_Tactic_SplitIfs___elabRules_Mathlib_Tactic_splitIfs_1

Lean4

@[tactic Mathlib.Tactic.splitIfs]
public meta def _aux_Mathlib_Tactic_SplitIfs___elabRules_Mathlib_Tactic_splitIfs_1 : Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| split_ifs$[$loc:location]?$[ with $withArg*]?) =>
    let loc :=
      match loc with
      | none => Location.targets #[] true
      | some loc => expandLocation loc
    let names :=
      match withArg with
      | none => []
      | some args => args.toList
    withMainContext do
      let names ← IO.mkRef names
      splitIfsCore loc names []
      for name in ← names.get do
        logWarningAt name m! "unused name: {name}"
  | _ => no_error_if_unused% throwUnsupportedSyntax✝

Похожие утверждения