isOk

Mathlib.Tactic.ITauto

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ITauto.isOk

Lean4

/-- Convert a value-with-success to an optional value. -/
def isOk : (Bool × Proof) × Nat → Option (Proof × Nat)
  | ((false, _), _) => none
  | ((true, p), n) => some (p, n)

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

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

Разделы

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

Аффилиация

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