Branch

Mathlib.Tactic.Linarith.Datatypes

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

Lean4

/-- Some preprocessors perform branching case splits. A `Branch` is used to track one of these case
splits. The first component, an `MVarId`, is the goal corresponding to this branch of the split,
given as a metavariable. The `List Expr` component is the list of hypotheses for `linarith`
in this branch.
-/
def Branch : Type :=
  MVarId × List Expr

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

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

Разделы

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

Аффилиация

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