Definitionadvanced
Brzozowski derivative of a regular expression
Also called Brzozowski derivative, derivative of a regex with respect to a symbol.
The expression for the suffixes after reading a symbol a, defined by structural recursion.
The expression for the suffixes after reading a symbol a, defined by structural recursion.
About this page
The build computes these levels from the evidence in the repository. Each row says what the next level needs. Read what the levels mean.
| Ladder | Level | What the next level needs |
|---|---|---|
| Human proof | H0 no proof |
|
| Lean | L0 no Lean part |
|
| Visual | V0 none |
|
| Writing | W0 stub |
|
Tag RMWSPE Edit this page History Report an error