package dolmen
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=80fc33ae81817a79c6e6b2f6c01c4cfcc0af02bfe4d2d1b87cf70b84cdde3928
sha512=3a44a99bce871161bc70cf909c813e9e6c91c590873cbc163c69b2ec90ab5be65bf0bf45430bc8d00d85d75cf0af004b06b8f5f1c9d4d47c8a30ab9f28762c04
doc/dolmen.std/Dolmen_std/Namespace/index.html
Module Dolmen_std.NamespaceSource
Type and std functions
type value = | Integer(*Integers (in base 10 notation), e.g.
*)"123456789"| Rational(*Rational (using quotient notation with '/'), e.g.
*)"123/456"| Real(*Real (using decimal floating point notation with exponent), e.g.
*)"123.456e789"| Binary(*Bitvector in binary notation, e.g.
*)"0b011010111010"| Hexadecimal(*Bitvector in hexadecimal notation, e.g.
*)"0x9a23e5f"| Bitvector(*Bitvector litteral.
*)| String(*String litterals.
*)
Types of lexical values typically encountered.
type t = | Var(*Namespace for variables. Not all variables are necessarily in this namespace, but ids in this namespace must be variables.
*)| Sort(*Namepsace for sorts and types (only used in smtlib)
*)| Term(*Most used namespace, used for terms in general (and types outside smtlib).
*)| Attr(*Namespace for attributes (also called annotations).
*)| Decl(*Namespace used for naming declarations/definitions/statements...
*)| Track(*Namespace used to track specific values throughout some files.
*)| Value of value(*The identifier is a value, encoded in a string. Examples include arithmetic constants (e.g.
*)"123456", "123/456", "123.456e789"), bitvectors (i.e. binary notation), etc...
Namespaces, used to record the lexical scop in which an identifier was parsed.
Printing function.