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

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