Languages #
This file contains the definition and operations on formal languages over an alphabet. Note strings are implemented as lists over the alphabet. The operations in this file define a Kleene algebra over the languages.
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- language.inhabited = {default := 0}
@[protected, instance]
The sum of two languages is the union of
@[protected, instance]
Equations
@[protected, instance]
Equations
- language.semiring = {add := has_add.add language.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul._default 0 has_add.add language.semiring._proof_4 language.semiring._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul language.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid_with_zero.npow._default 1 has_mul.mul language.semiring._proof_16 language.semiring._proof_17, npow_zero' := _, npow_succ' := _}