mkCCHCongrWithArity

Mathlib.Tactic.CC.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.mkCCHCongrWithArity

Lean4

/-- Automatically generated congruence lemma based on heterogeneous equality.

This returns an annotated version of the result from `Lean.Meta.mkHCongrWithArity`. -/
def mkCCHCongrWithArity (fn : Expr) (nargs : Nat) : MetaM (Option CCCongrTheorem) := do
  let eqCongr ←
    try
      mkHCongrWithArity fn nargs
    catch _ =>
      return none
  return
    some
      { eqCongr with
        heqResult := true
        hcongrTheorem := true }

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

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

Разделы

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

Аффилиация

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