def Regex.Data.Expr.nullOnly (expr : Expr) : Bool

Equations

• Regex.Data.Expr.empty.nullOnly = true
• Regex.Data.Expr.epsilon.nullOnly = true
• (Regex.Data.Expr.anchor a).nullOnly = true
• (Regex.Data.Expr.char a).nullOnly = false
• (Regex.Data.Expr.classes a).nullOnly = false
• (Regex.Data.Expr.group a e).nullOnly = e.nullOnly
• (e₁.concat e₂).nullOnly = (e₁.nullOnly && e₂.nullOnly)
• (e₁.alternate e₂).nullOnly = (e₁.nullOnly && e₂.nullOnly)
• e.star.nullOnly = e.nullOnly

def Regex.Data.Expr.firstChar (expr : Expr) : Option Char

Equations

• Regex.Data.Expr.empty.firstChar = none
• Regex.Data.Expr.epsilon.firstChar = none
• (Regex.Data.Expr.anchor a).firstChar = none
• (Regex.Data.Expr.char a).firstChar = some a
• (Regex.Data.Expr.classes a).firstChar = none
• (Regex.Data.Expr.group a e).firstChar = e.firstChar
• (e₁.concat e₂).firstChar = if e₁.nullOnly = true then e₂.firstChar else e₁.firstChar
• (e₁.alternate e₂).firstChar = do let c₁ ← e₁.firstChar let c₂ ← e₂.firstChar if c₁ = c₂ then some c₁ else none
• e.star.firstChar = none