rflTac

Mathlib.Tactic.Relation.Rfl

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.rflTac

Lean4

/-- This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
-/
def rflTac : TacticM Unit :=
  withMainContext do
    liftMetaFinishingTactic (·.applyRfl)

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

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

Разделы

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

Аффилиация

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