isValue

Mathlib.Tactic.CC.Datatypes

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

Lean4

/-- Return true if `e` represents a constant value (numeral, character, or string). -/
def isValue (e : Expr) : Bool :=
  e.int?.isSome || e.isCharLit || e.isStringLit

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

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

Разделы

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

Аффилиация

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