Rewrites — Mathlib

Lean4
/-- Inductive definition of a single application of a given context-free rule `r` to a string `u`;
`r.Rewrites u v` means that the `r` sends `u` to `v` (there may be multiple such strings `v`). -/
inductive Rewrites (r : ContextFreeRule T N) : List (Symbol T N) → List (Symbol T N) → Prop/--
The replacement is at the start of the remaining string. -/

  | head (s : List (Symbol T N)) : r.Rewrites (Symbol.nonterminal r.input :: s) (r.output ++ s)/--
There is a replacement later in the string. -/

  | cons (x : Symbol T N) {s₁ s₂ : List (Symbol T N)} (hrs : Rewrites r s₁ s₂) : r.Rewrites (x :: s₁) (x :: s₂)
Похожие утверждения