toDeclaration!

Mathlib.Lean.Expr.Basic

URI: https://scilib.ai/kg/mathlib#Lean.ConstantInfo.toDeclaration!

Lean4

/-- Turn a `ConstantInfo` into a declaration. -/
def toDeclaration! : ConstantInfo → Declaration
  | defnInfo info => Declaration.defnDecl info
  | thmInfo info => Declaration.thmDecl info
  | axiomInfo info => Declaration.axiomDecl info
  | opaqueInfo info => Declaration.opaqueDecl info
  | quotInfo _ => panic! "toDeclaration for quotInfo not implemented"
  | inductInfo _ => panic! "toDeclaration for inductInfo not implemented"
  | ctorInfo _ => panic! "toDeclaration for ctorInfo not implemented"
  | recInfo _ => panic! "toDeclaration for recInfo not implemented"

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

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

Разделы

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

Аффилиация

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