Zulip Chat Archive

Stream: general

Topic: automata theorem

Yunlong LIN (Mar 27 2022 at 06:19):

I am a freshman in lean and currently working on the automata theorem,
could anyone help me with the the line 92 and line 112 or give me some instructions about what lemmas I need to prove in the repo below, which related to translating from DFA to NFA.
https://bitbucket.org/yunlong_0125/project/src/main/code/src/new_project.lean

Yaël Dillies (Mar 27 2022 at 09:22):

Hey! Have you read through the mathlib implementation? docs#DFA, docs#NFA

Yaël Dillies (Mar 27 2022 at 09:23):

I also have some stuff over at branch#regex_nfa that I meant to PR a while back but never got round to doing.

Yunlong LIN (Mar 27 2022 at 09:51):

Yeah, I read it, but it seems to use different definitions with me.

Yunlong LIN (Mar 27 2022 at 10:05):

I just wonder how to do it based on this definition. Could you please help me to take a look on it?

Yaël Dillies (Mar 27 2022 at 10:16):

I will have a look later :smile:

Last updated: Dec 20 2023 at 11:08 UTC