matches'

Mathlib.Computability.RegularExpressions

URI: https://scilib.ai/kg/mathlib#RegularExpression.matches'

Lean4

/-- `matches' P` provides a language which contains all strings that `P` matches.

Not named `matches` since that is a reserved word.
-/
@[simp]
def matches' : RegularExpression α → Language α
  | 0 => 0
  | 1 => 1
  | char a => { [a] }
  | P + Q => P.matches' + Q.matches'
  | P * Q => P.matches' * Q.matches'
  | star P => P.matches'∗

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

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

Разделы

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

Аффилиация

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