Module String.RegLan

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

val empty : t

The empty regular language.

val all : t

The language that contains all strings

val allchar : t

The language that contains all strings of length 1

val of_string : t -> t

Singleton language containing a single string.

val 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.

val concat : t -> t -> t

Language concatenation.

val union : t -> t -> t

Language union.

val inter : t -> t -> t

language intersection.

val star : t -> t

Kleene closure.

val cross : t -> t

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

val complement : t -> t

Complement.

val diff : t -> t -> t

Difference

val option : t -> t

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

val power : int -> t -> t

power n e is n-th power of e.

val loop : int -> int -> t -> t

Loop. See SMTLIb documentation.