Langlib
Langlib
.
Classes
.
DeterministicContextFree
.
Examples
.
SingletonWord
Search
return to top
source
Imports
Init
Langlib.Classes.DeterministicContextFree.Definition
Langlib.Classes.Regular.Examples.SingletonWord
Langlib.Classes.Regular.Inclusion.DeterministicContextFree
Imported by
singletonWordLanguage_is_DCF
The singleton-word language is deterministic context-free
#
source
theorem
singletonWordLanguage_is_DCF
{
T
:
Type
}
[
Fintype
T
]
(
w
:
List
T
)
:
is_DCF
(
singletonWordLanguage
w
)
The singleton-word language
{w}
is deterministic context-free.
Langlib