package dolmen
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=3ee4b4b028b18ab0066cb4648fa14cd4d628a3afd79455f85fb796a9969ac80c
sha512=06d455f0221814dae44d9d8614cab7c1d4fb43a383e603a92ffc9cf4a753d42c5f2a0f3c5ae64aa6cf02da769c4666b130443ae2cf8fa0918c906d46e0caec9a
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.