feat: proof of Myhill-Nerode theorem for DFAs#491

Open

akhilesh-balaji wants to merge 17 commits intoleanprover:mainfrom

akhilesh-balaji:myhill-nerode

Commits on Apr 3, 2026

feat: prove myhill-nerode equivalence classes
akhilesh-balaji
committed

Commits on Apr 7, 2026

feat: proof of number of states of minimal DFA for a language
akhilesh-balaji
committed

Commits on Apr 8, 2026

Commits on Apr 13, 2026

Commits on Apr 14, 2026

Merge branch 'leanprover:main' into myhill-nerode
akhilesh-balaji
authored

Commits on Apr 15, 2026

Commits on Apr 20, 2026

fix linter errors and remove some unnecessary @[simp]
ctchou
committed

Commits on Apr 21, 2026

Merge remote-tracking branch 'upstream/main' into myhill-nerode
ctchou
committed