Langlib
Langlib
.
Classes
.
Indexed
.
Examples
.
SingletonWord
Search
return to top
source
Imports
Init
Langlib.Classes.Indexed.Definition
Langlib.Classes.ContextFree.Examples.SingletonWord
Langlib.Classes.ContextFree.Inclusion.Indexed
Imported by
singletonWordLanguage_is_Indexed
The singleton-word language is indexed
#
source
theorem
singletonWordLanguage_is_Indexed
{
T
:
Type
}
[
Fintype
T
]
(
w
:
List
T
)
:
is_Indexed
(
singletonWordLanguage
w
)
The singleton-word language
{w}
is indexed.