def Regex.Data.Expr.tags : Expr → Finset ℕ

Equations

• Regex.Data.Expr.empty.tags = ∅
• Regex.Data.Expr.epsilon.tags = ∅
• (Regex.Data.Expr.anchor a).tags = ∅
• (Regex.Data.Expr.char a).tags = ∅
• (Regex.Data.Expr.classes a).tags = ∅
• (Regex.Data.Expr.group tag e).tags = {tag} ∪ e.tags
• (e₁.alternate e₂).tags = e₁.tags ∪ e₂.tags
• (e₁.concat e₂).tags = e₁.tags ∪ e₂.tags
• e.star.tags = e.tags

def Regex.Data.Expr.Disjoint : Expr → Prop

Equations

• Regex.Data.Expr.empty.Disjoint = True
• Regex.Data.Expr.epsilon.Disjoint = True
• (Regex.Data.Expr.anchor a).Disjoint = True
• (Regex.Data.Expr.char a).Disjoint = True
• (Regex.Data.Expr.classes a).Disjoint = True
• (Regex.Data.Expr.group tag e).Disjoint = (tag ∉ e.tags ∧ e.Disjoint)
• (e₁.alternate e₂).Disjoint = (e₁.Disjoint ∧ e₂.Disjoint)
• (e₁.concat e₂).Disjoint = (e₁.Disjoint ∧ e₂.Disjoint)
• e.star.Disjoint = e.Disjoint

theorem Regex.Data.Expr.Captures.mem_tags_of_mem_groups {e : Expr} {it it' : String.Iterator} {groups : CaptureGroups} (c : Captures it it' groups e) (tag : ℕ) (first last : String.Pos) : (tag, first, last) ∈ groups → tag ∈ e.tags