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

∫ Утверждение Mathlib

_aux_Mathlib_Tactic_IrreducibleDef_elabRulesprivate_Mathlib_Tactic_IrreducibleDef_0_Lean_Elab_Command_commandStop_at_first_error___1

Mathlib.Tactic.IrreducibleDef

URI: https://scilib.ai/kg/mathlib#Lean.Elab.Command._aux_Mathlib_Tactic_IrreducibleDef___elabRules__private_Mathlib_Tactic_IrreducibleDef_0_Lean_Elab_Command_commandStop_at_first_error___1

← MathLib Explorer

Lean4

@[command_elab _private.Mathlib.Tactic.IrreducibleDef.0.Lean.Elab.Command.commandStop_at_first_error__]
public meta def
  _aux_Mathlib_Tactic_IrreducibleDef___elabRules__private_Mathlib_Tactic_IrreducibleDef_0_Lean_Elab_Command_commandStop_at_first_error___1 :
    Lean.Elab.Command.CommandElab✝ := fun
  |
  `(stop_at_first_error$[
        $cmds]*) =>
    do
    for cmd in cmds do
      elabCommand cmd.raw
      if (← get).messages.hasErrors then
        break
  | _ => no_error_if_unused% throwUnsupportedSyntax✝

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

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

Разделы

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

Аффилиация

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

© 2026 SciLib Lab · ФИЦ ИУ РАН. Все права защищены. Контакты: info@scilibai.ru