The empty regular language.

The language that contains all strings.

The language that contains all strings of length 1.

Singleton language containing a single string.

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.

Language concatenation.

Language union.

Language intersection.

Language difference.

Kleene closure.

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

Language complement.

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

power n e is n-th power of e.

Loop. See SMTLIb documentation.