Zulip Chat Archive
Stream: mathlib4
Topic: Language.IsRegular infinite alphabets?
Owen Kahn (Nov 06 2024 at 00:49):
Related to #mathlib4 > Rename DFA?: should Language.IsRegular require the alphabet to be finite? This is often but not always given as part of the definition; I couldn’t say offhand which theorems depend on this assumption.
Kim Morrison (Nov 06 2024 at 05:26):
Kim Morrison (Nov 06 2024 at 05:27):
We tend not to put "side conditions" on definitions if they can live on the theorems instead.
Owen Kahn (Nov 06 2024 at 15:48):
Got, it, thanks! I'll keep that in mind as I read the library
Last updated: May 02 2025 at 03:31 UTC