inductive Regex.Data.Expr.Captures {s : String} : s.ValidPos → s.ValidPos → CaptureGroups s → Expr → Prop

• char {s : String} {p : s.ValidPos} {c : Char} (ne : p ≠ s.endValidPos) (eq : p.get ne = c) : Captures p (p.next ne) CaptureGroups.empty (Expr.char c)
• sparse {s : String} {p : s.ValidPos} {cs : Classes} (ne : p ≠ s.endValidPos) (h : p.get ne ∈ cs) : Captures p (p.next ne) CaptureGroups.empty (classes cs)
• epsilon {s : String} {p : s.ValidPos} : Captures p p CaptureGroups.empty Expr.epsilon
• anchor {s : String} {p : s.ValidPos} {anchor : Anchor} (h : Anchor.test p anchor = true) : Captures p p CaptureGroups.empty (Expr.anchor anchor)
• group {s : String} {p p' : s.ValidPos} {groups : CaptureGroups s} {tag : ℕ} {e : Expr} (cap : Captures p p' groups e) : Captures p p' (CaptureGroups.group tag p p' groups) (Expr.group tag e)
• alternateLeft {s : String} {p p' : s.ValidPos} {groups : CaptureGroups s} {e₁ e₂ : Expr} (cap : Captures p p' groups e₁) : Captures p p' groups (e₁.alternate e₂)
• alternateRight {s : String} {p p' : s.ValidPos} {groups : CaptureGroups s} {e₁ e₂ : Expr} (cap : Captures p p' groups e₂) : Captures p p' groups (e₁.alternate e₂)
• concat {s : String} {p p' p'' : s.ValidPos} {groups₁ groups₂ : CaptureGroups s} {e₁ e₂ : Expr} (cap₁ : Captures p p' groups₁ e₁) (cap₂ : Captures p' p'' groups₂ e₂) : Captures p p'' (groups₁.concat groups₂) (e₁.concat e₂)
• starEpsilon {s : String} {p : s.ValidPos} {greedy : Bool} {e : Expr} : Captures p p CaptureGroups.empty (star greedy e)
• starConcat {s : String} {p p' p'' : s.ValidPos} {groups₁ groups₂ : CaptureGroups s} {greedy : Bool} {e : Expr} (cap₁ : Captures p p' groups₁ e) (cap₂ : Captures p' p'' groups₂ (star greedy e)) : Captures p p'' (groups₁.concat groups₂) (star greedy e)

theorem Regex.Data.Expr.Captures.le {s : String} {p p' : s.ValidPos} {groups : CaptureGroups s} {e : Expr} (c : Captures p p' groups e) : p ≤ p'