package dolmen_type

  1. Overview
  2. Docs
package dolmen_type
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

val empty : Type.T.t

The empty regular language.

val all : Type.T.t

The language that contains all strings

val allchar : Type.T.t

The language that contains all strings of length 1

val of_string : Type.T.t -> Type.T.t

Singleton language containing a single string.

val range : Type.T.t -> Type.T.t -> Type.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 : Type.T.t -> Type.T.t -> Type.T.t

Language concatenation.

val union : Type.T.t -> Type.T.t -> Type.T.t

Language union.

val inter : Type.T.t -> Type.T.t -> Type.T.t

language intersection.

val star : Type.T.t -> Type.T.t

Kleene closure.

val cross : Type.T.t -> Type.T.t

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

val complement : Type.T.t -> Type.T.t

Complement.

val diff : Type.T.t -> Type.T.t -> Type.T.t

Difference

val option : Type.T.t -> Type.T.t

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

val power : int -> Type.T.t -> Type.T.t

power n e is n-th power of e.

val loop : int -> int -> Type.T.t -> Type.T.t

Loop. See SMTLIb documentation.