Module String.RegLanSource

Sub-module used for namespacing for the regular language part of the theory requirements.

Sourceval empty : t

The empty regular language.

Sourceval all : t

The language that contains all strings

Sourceval allchar : t

The language that contains all strings of length 1

Sourceval of_string : t -> t

Singleton language containing a single string.

Sourceval range : t -> t -> t

range s1 s2 is the language containing all singleton strings (i.e. string of length 1) that are lexicographically beetween s1 and s2, **assuming s1 and s2 are singleton strings**. Else it is the empty language.

Sourceval concat : t -> t -> t

Language concatenation.

Sourceval union : t -> t -> t

Language union.

Sourceval inter : t -> t -> t

language intersection.

Sourceval star : t -> t

Kleene closure.

Sourceval cross : t -> t

Kleene cross. cross e abbreviates concat e (star e)

Sourceval complement : t -> t

Complement.

Sourceval diff : t -> t -> t

Difference

Sourceval option : t -> t

Option. option e abbreviates union e (of_string "")

Sourceval power : int -> t -> t

power n e is n-th power of e.

Sourceval loop : int -> int -> t -> t

Loop. See SMTLIb documentation.