inductive Regex.Data.Expr.Captures : String.Iterator → String.Iterator → CaptureGroups → Expr → Prop

• char {it : String.Iterator} {l : List Char} {c : Char} {r : List Char} (vf : String.Iterator.ValidFor l (c :: r) it) : Captures it it.next CaptureGroups.empty (Expr.char c)
• sparse {it : String.Iterator} {l : List Char} {c : Char} {r : List Char} {cs : Classes} (vf : String.Iterator.ValidFor l (c :: r) it) (h : c ∈ cs) : Captures it it.next CaptureGroups.empty (classes cs)
• epsilon {it : String.Iterator} (v : it.Valid) : Captures it it CaptureGroups.empty Expr.epsilon
• anchor {it : String.Iterator} {anchor : Anchor} (v : it.Valid) (h : Anchor.test it anchor = true) : Captures it it CaptureGroups.empty (Expr.anchor anchor)
• group {it it' : String.Iterator} {groups : CaptureGroups} {tag : ℕ} {e : Expr} (cap : Captures it it' groups e) : Captures it it' (CaptureGroups.group tag it.pos it'.pos groups) (Expr.group tag e)
• alternateLeft {it it' : String.Iterator} {groups : CaptureGroups} {e₁ e₂ : Expr} (cap : Captures it it' groups e₁) : Captures it it' groups (e₁.alternate e₂)
• alternateRight {it it' : String.Iterator} {groups : CaptureGroups} {e₁ e₂ : Expr} (cap : Captures it it' groups e₂) : Captures it it' groups (e₁.alternate e₂)
• concat {it it' it'' : String.Iterator} {groups₁ groups₂ : CaptureGroups} {e₁ e₂ : Expr} (cap₁ : Captures it it' groups₁ e₁) (cap₂ : Captures it' it'' groups₂ e₂) : Captures it it'' (groups₁.concat groups₂) (e₁.concat e₂)
• starEpsilon {it : String.Iterator} {e : Expr} (v : it.Valid) : Captures it it CaptureGroups.empty e.star
• starConcat {it it' it'' : String.Iterator} {groups₁ groups₂ : CaptureGroups} {e : Expr} (cap₁ : Captures it it' groups₁ e) (cap₂ : Captures it' it'' groups₂ e.star) : Captures it it'' (groups₁.concat groups₂) e.star

theorem Regex.Data.Expr.Captures.validL {it it' : String.Iterator} {groups : CaptureGroups} {e : Expr} (c : Captures it it' groups e) : it.Valid

theorem Regex.Data.Expr.Captures.validR {it it' : String.Iterator} {groups : CaptureGroups} {e : Expr} (c : Captures it it' groups e) : it'.Valid

theorem Regex.Data.Expr.Captures.toString_eq {it it' : String.Iterator} {groups : CaptureGroups} {e : Expr} (c : Captures it it' groups e) : it'.toString = it.toString

theorem Regex.Data.Expr.Captures.le_pos {it it' : String.Iterator} {groups : CaptureGroups} {e : Expr} (c : Captures it it' groups e) : it.pos ≤ it'.pos