mkComp

Mathlib.Tactic.HigherOrder

URI: https://scilib.ai/kg/mathlib#Tactic.mkComp

Lean4

/-- `mkComp v e` checks whether `e` is a sequence of nested applications `f (g (h v))`, and if so,
returns the expression `f ∘ g ∘ h`. If `e = v` it returns `id`. -/
def mkComp (v : Expr) : Expr → MetaM Expr
  | .app f e =>
    if e.equal v then return f
    else do
      if v.occurs f then
        throwError"mkComp failed occurs check"
      let e' ← mkComp v e
      mkAppM ``Function.comp #[f, e']
  | e => do
    guard (e.equal v)
    let t ← inferType e
    mkAppOptM ``id #[t]

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

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

Разделы

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

Аффилиация

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