linarithTraceProofs

Mathlib.Tactic.Linarith.Datatypes

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

Lean4

/-- A shorthand for tracing the types of a list of proof terms
when the `trace.linarith` option is set to true.
-/
def linarithTraceProofs {α} [ToMessageData α] (s : α) (l : List Expr) : MetaM Unit := do
  if ← isTracingEnabledFor `linarith then
    addRawTrace <| .trace { cls := `linarith } (toMessageData s) #[← linarithGetProofsMessage l]

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

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

Разделы

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

Аффилиация

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