package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type value =
  1. | Vconstr of Expr.rsymbol * field list
  2. | Vtuple of value list
  3. | Vbigint of BigInt.t
  4. | Vint of int
  5. | Vbool of bool
  6. | Vstring of string
  7. | Vvoid
  8. | Varray of value array
  9. | Vmatrix of value array array
  10. | Vref of value ref
and field =
  1. | Fimmutable of value
  2. | Fmutable of value ref
exception CannotReduce
exception Raised of Ity.xsymbol * value option * Expr.rsymbol list
val value_of_term : Decl.known_map -> Term.term -> value
val term_of_value : value -> Term.term
OCaml

Innovation. Community. Security.