isInterpretedValue

Mathlib.Tactic.CC.Datatypes

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

Lean4

/-- Return true if `e` represents a value (nat/int numeral, character, or string).

In addition to the conditions in `Mathlib.Tactic.CC.isValue`, this also checks that
kernel computation can compare the values for equality. -/
def isInterpretedValue (e : Expr) : MetaM Bool := do
  if e.isCharLit || e.isStringLit then
    return true
  else if e.int?.isSome then
    let type ← inferType e
    pureIsDefEq type (.const ``Nat []) <||> pureIsDefEq type (.const ``Int [])
  else
    return false

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

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

Разделы

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

Аффилиация

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