Karl Palmskog (Nov 25 2021 at 12:18): Karl Palmskog (Nov 25 2021 at 12:18):@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?
Karl Palmskog (Nov 25 2021 at 14:05):Right. OK, then I will do a PR with in_residual and friends.
Karl Palmskog (Nov 25 2021 at 15:03):sigh, the Reglang CI failed due to Alpine Linux network error
Last updated: Jun 03 2023 at 17:29 UTC