_aux_Mathlib_Tactic_CategoryTheory_Slice___macroRules_sliceRHS_1

Mathlib.Tactic.CategoryTheory.Slice

URI: https://scilib.ai/kg/mathlib#_aux_Mathlib_Tactic_CategoryTheory_Slice___macroRules_sliceRHS_1

Lean4

@[macro sliceRHS]
public meta def _aux_Mathlib_Tactic_CategoryTheory_Slice___macroRules_sliceRHS_1 : Macro✝ := fun
  | `(tactic| slice_rhs $a $b => $seq) =>
    `(tactic| conv => rhs; slice $a $b; ($seq:convSeq))
      /- Porting note: update when `add_tactic_doc` is supported` -/
      -- add_tactic_doc
      --   { Name := "slice"
      --     category := DocCategory.tactic
      --     declNames := [`tactic.interactive.sliceLHS, `tactic.interactive.sliceRHS]
      --     tags := ["category theory"] }
      --

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru