package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type variable = string

type bv_value =

| Bv_int of string
| Bv_sharp of string

type simple_value =

| String of string
| Integer of string
| Decimal of string * string
| Fraction of string * string
| Float of Model_parser.float_type
| Other of string
| Bitvector of bv_value
| Boolean of bool

type array =

| Array_var of variable
| Const of term
| Store of array * term * term

and term =

| Sval of simple_value
| Apply of string * term list
| Array of array
| Cvc4_Variable of variable
| Function_Local_Variable of variable
| Variable of variable
| Ite of term * term * term * term
| Record of string * (string * term) list
| To_array of term
| Trees of (string * term) list

type definition =

| Function of (variable * string option) list * term
| Term of term
| 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