@Christian Doczkal what do you think of the following quite weak lemmas from regexp-Brzozowski, are they possibly worth adding to reglang? I guess they are mostly just restating the meaning of dot, compl, residual.

```
Lemma in_dot u : (u \in dot) = (size u == 1).
Proof. by []. Qed.
Lemma in_compl L v : (v \in compl L) = (v \notin L).
Proof. by []. Qed.
Lemma residualE x L u : (u \in residual x L) = (x :: u \in L).
Proof. by []. Qed.
```

Yes, sure, feel free to add/move them to reglang. I suppose that, like other `in_`

lemmas in mathcomp, they are mainly useful in their right-to-left direction. For consistency, the last one should probably be named `in_residual`

, right?

Right. OK, then I will do a PR with `in_residual`

and friends.

sigh, the Reglang CI failed due to Alpine Linux network error

Last updated: May 25 2024 at 20:01 UTC