TriggerCondition

Mathlib.Tactic.TacticAnalysis

URI: https://scilib.ai/kg/mathlib#Mathlib.TacticAnalysis.TriggerCondition

Lean4

/-- The condition is returned from the `.trigger` function to indicate which sublists of a
tactic sequence to test.

The `context` field can be used to accumulate data between different invocations of `.trigger`.
-/
inductive TriggerCondition (ctx : Type _)/--
`skip` means that the current tactic and the ones before it will be discarded. -/

  | skip/-- `continue` means to accumulate the current tactic, but not yet run the test on it. -/

  | continue (context : ctx)/-- `accept` means to run the test on the sequence of `.continue`s up to this `.accept`. -/

  | accept (context : ctx)
  deriving BEq

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

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

Разделы

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

Аффилиация

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