commandCompile_inductive%_

Mathlib.Util.CompileInductive

URI: https://scilib.ai/kg/mathlib#Mathlib.Util.commandCompile_inductive%_

Lean4

/-- `compile_inductive% Foo` creates compiled code for the recursor `Foo.rec`,
so that `Foo.rec` can be used in a definition
without having to mark the definition as `noncomputable`.
-/
@[command_parser 1000]
public meta def «commandCompile_inductive%_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Util.«commandCompile_inductive%_» 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "compile_inductive% ") (ParserDescr.const✝ `ident))

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

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

Разделы

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

Аффилиация

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