From 673496b95fb38c9644c1ded4207868047cc707f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Wed, 9 Aug 2023 12:19:15 +0200 Subject: [PATCH] docs(Computability/NFA) --- Mathlib/Computability/NFA.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Computability/NFA.lean b/Mathlib/Computability/NFA.lean index 65480352e29d0..13f58ecc80f06 100644 --- a/Mathlib/Computability/NFA.lean +++ b/Mathlib/Computability/NFA.lean @@ -15,7 +15,7 @@ which determines whether a string (implemented as a list over an arbitrary alpha set by evaluating the string over every possible path. We show that DFA's are equivalent to NFA's however the construction from NFA to DFA uses an exponential number of states. -Note that this definition allows for Automaton with infinite states, a `Fintype` instance must be +Note that this definition allows for Automaton with infinite states; a `Fintype` instance must be supplied for true NFA's. -/ @@ -30,7 +30,7 @@ universe u v set_option linter.uppercaseLean3 false /-- An NFA is a set of states (`σ`), a transition function from state to state labelled by the - alphabet (`step`), a starting state (`start`) and a set of acceptance states (`accept`). + alphabet (`step`), a set of starting states (`start`) and a set of acceptance states (`accept`). Note the transition function sends a state to a `Set` of states. These are the states that it may be sent to. -/ structure NFA (α : Type u) (σ : Type v) where