Kind

Mathlib.Tactic.Widget.LibraryRewrite

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

Lean4

/-- The kind of rewrite -/
inductive Kind where/-- A rewrite with a local hypothesis -/

  | hypothesis/-- A rewrite with a lemma from the current file -/

  | fromFile/-- A rewrite with a lemma from an imported file -/

  | fromCache

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

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

Разделы

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

Аффилиация

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