package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type variable = string
type bv_value =
  1. | Bv_int of string
  2. | Bv_sharp of string
type simple_value =
  1. | String of string
  2. | Integer of string
  3. | Decimal of string * string
  4. | Fraction of string * string
  5. | Float of Model_parser.float_type
  6. | Other of string
  7. | Bitvector of bv_value
  8. | Boolean of bool
type array =
  1. | Array_var of variable
  2. | Const of term
  3. | Store of array * term * term
and term =
  1. | Sval of simple_value
  2. | Apply of string * term list
  3. | Array of array
  4. | Cvc4_Variable of variable
  5. | Function_Local_Variable of variable
  6. | Variable of variable
  7. | Ite of term * term * term * term
  8. | Record of string * (string * term) list
  9. | To_array of term
  10. | Trees of (string * term) list
type definition =
  1. | Function of (variable * string option) list * term
  2. | Term of term
  3. | Noelement
val add_element : (string * definition) option -> definition Wstdlib.Mstr.t -> definition Wstdlib.Mstr.t
val make_local : (variable * string option) list -> term -> term
val substitute : (string * term) list -> term -> term
OCaml

Innovation. Community. Security.