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)
• (Regex.Data.Expr.star a e).nullOnly = e.nullOnly

def Regex.Data.Expr.firstChars (maxSize : Nat) (expr : Expr) : Option (Std.HashSet Char)

Equations

• One or more equations did not get rendered due to their size.
• Regex.Data.Expr.firstChars maxSize Regex.Data.Expr.empty = do let y ← none (fun (cs : Std.HashSet Char) => do guard (cs.size ≤ maxSize) pure cs) y
• Regex.Data.Expr.firstChars maxSize Regex.Data.Expr.epsilon = do let y ← none (fun (cs : Std.HashSet Char) => do guard (cs.size ≤ maxSize) pure cs) y
• Regex.Data.Expr.firstChars maxSize (Regex.Data.Expr.anchor a) = do let y ← none (fun (cs : Std.HashSet Char) => do guard (cs.size ≤ maxSize) pure cs) y
• Regex.Data.Expr.firstChars maxSize (Regex.Data.Expr.char a) = do let y ← some {a} (fun (cs : Std.HashSet Char) => do guard (cs.size ≤ maxSize) pure cs) y
• Regex.Data.Expr.firstChars maxSize (Regex.Data.Expr.classes a) = do let y ← none (fun (cs : Std.HashSet Char) => do guard (cs.size ≤ maxSize) pure cs) y
• Regex.Data.Expr.firstChars maxSize (e₁.alternate e₂) = do let cs₁ ← Regex.Data.Expr.firstChars maxSize e₁ let cs₂ ← Regex.Data.Expr.firstChars maxSize e₂ pure (cs₁.union cs₂)
• Regex.Data.Expr.firstChars maxSize (Regex.Data.Expr.star a e) = do let y ← none (fun (cs : Std.HashSet Char) => do guard (cs.size ≤ maxSize) pure cs) y