inductive Regex.Data.CaptureGroups (s : String) : Type

Groups captured by a regex match.

• For .group tag first last rest, the group with tag tag starts at position first and ends at position last. It will overwrite the positions with the same tag in rest.
• .concat g₁ g₂ joins the capture groups for concatenations by preferring the groups in g₂ over g₁. (Last write wins.)

• empty {s : String} : CaptureGroups s
• group {s : String} (tag : Nat) (first last : s.ValidPos) (rest : CaptureGroups s) : CaptureGroups s
• concat {s : String} (g₁ g₂ : CaptureGroups s) : CaptureGroups s

def Regex.Data.CaptureGroups.mem {s : String} (groups : CaptureGroups s) (group : Nat × s.ValidPos × s.ValidPos) : Prop

Equations

• Regex.Data.CaptureGroups.empty.mem group = False
• (Regex.Data.CaptureGroups.group tag first last rest).mem group = (tag = group.fst ∧ first = group.snd.fst ∧ last = group.snd.snd ∨ rest.mem group)
• (g₁.concat g₂).mem group = (g₁.mem group ∨ g₂.mem group)

instance Regex.Data.CaptureGroups.instMembershipProdNatValidPos {s : String} : Membership (Nat × s.ValidPos × s.ValidPos) (CaptureGroups s)

Equations

• Regex.Data.CaptureGroups.instMembershipProdNatValidPos = { mem := Regex.Data.CaptureGroups.mem }

@[simp]

theorem Regex.Data.CaptureGroups.mem_empty {s : String} {group : Nat × s.ValidPos × s.ValidPos} : group ∈ empty ↔ False

@[simp]

theorem Regex.Data.CaptureGroups.mem_group {s : String} {group : Nat × s.ValidPos × s.ValidPos} {tag : Nat} {first last : s.ValidPos} {rest : CaptureGroups s} : group ∈ CaptureGroups.group tag first last rest ↔ group = (tag, first, last) ∨ group ∈ rest

@[simp]

theorem Regex.Data.CaptureGroups.mem_concat {s : String} {group : Nat × s.ValidPos × s.ValidPos} {g₁ g₂ : CaptureGroups s} : group ∈ g₁.concat g₂ ↔ group ∈ g₁ ∨ group ∈ g₂