package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Make.TypesSource

Sourceval int : ty

int represents the integer type.

Sourceval real : ty

real represents the real number type.

Sourceval bool : ty

bool represents the Boolean type.

Sourceval string : ty

string represents the string type.

Sourceval bitv : int -> ty

bitv n represents a bitvector type of width n.

Sourceval float : int -> int -> ty

float e s represents a floating-point type with exponent width e and significand width s.

Sourceval roundingMode : ty
Sourceval regexp : ty

regexp represents the regular expression type.

Sourceval ty : term -> ty

ty t retrieves the type of the term t.

Sourceval to_ety : ty -> Ty.t

to_ety ty converts the type ty to an smtml type representation.