package dolmen_type

  1. Overview
  2. Docs

Module Arrays.Smtlib2Source

Smtlib array builtins

Sourcetype arrays =
  1. | All
  2. | Only_int_int
  3. | Only_ints_real
  4. | Only_bitvec

The difference type of array restrictions that can be imposed by logics.

Sourcemodule Tff (Type : Tff_intf.S) (Ty : Dolmen.Intf.Ty.Smtlib_Array with type t := Type.Ty.t) (T : Dolmen.Intf.Term.Smtlib_Array with type t := Type.T.t) : sig ... end