_aux_Mathlib_Tactic_ITauto___macroRules_Mathlib_Tactic_ITauto_itauto!_1

Lean4

@[macro Mathlib.Tactic.ITauto.itauto!]
public meta def _aux_Mathlib_Tactic_ITauto___macroRules_Mathlib_Tactic_ITauto_itauto!_1 : Macro✝ := fun
  | `(tactic| itauto!) => `(tactic| itauto !)
  | `(tactic| itauto! *) => `(tactic| itauto ! *)
  | `(tactic| itauto! [$hs,*]) =>
    `(tactic| itauto ! [$hs,*])
      -- add_hint_tactic itauto

      -- add_tactic_doc
      --   { Name := "itauto"
      --     category := DocCategory.tactic
      --     declNames := [`tactic.interactive.itauto]
      --     tags := ["logic", "propositional logic", "intuitionistic logic", "decision procedure"] }

  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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