Zulip Chat Archive

Stream: mathlib4

Topic: computability

Arthur Correnson (Nov 30 2022 at 08:15):

Hi all ! I'd like to port the computability.DFA and computability.NFA modules to mathlib4 ^^. As far as I could tell, it's not being ported yet. Is it ok ?

Kevin Buzzard (Nov 30 2022 at 09:05):

Did you watch the video mentioned in the wiki? If all prerequisites are ported, and nobody claimed these files yet on the port status page then claim them and go ahead!

Yaël Dillies (Nov 30 2022 at 09:39):

I'm afraid you will need finiteness first.

Last updated: Dec 20 2023 at 11:08 UTC