package electrod

You can search for identifiers within the package.

in-package search v0.2.0

Formal analysis for the Electrod formal pivot language

Install

Dune Dependency

github.com Readme Changelog MPL-2.0 License Edit opam file Versions (10)

Authors

Maintainers

D

David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-0.3.2.tbz

sha256=c58502de17f5b8d739963b5b5d7c761883305bc2b6464fc37769aae4bb31a28c

sha512=bc15032cbda06b0eb64d55cc7800d6c992c0823bb86609ddc5e56744fd0c76ea25b4f4ad7cafdee6fcaa2f109e48ca99f4270919f9a2ea4c7bf53f30b0ee3677

doc/electrod.libelectrod/Libelectrod/Tuple/index.html

Module `Libelectrod.Tuple`Source

Tuples of atoms.

Sourcetype t

invariant: atoms <> empty

Sourceval of_list1 : Atom.t list -> t

Builds a tuple out of a non-empty list of atoms.

Sourceval tuple1 : Atom.t -> t

Builds a 1-tuple out of an atom.

Sourceval arity : t -> int

Returns the arity of the tuple.

Sourceval (@@@) : t -> t -> t

t1 @@@ t2 yields the concatenation of t1 followed by t2 (useful to compute the flat product of bounds/tuple sets).

Sourceval concat : t list -> t

Concatenation of a list of tuples. Fails if the list is empty.

Sourceval compare : t -> t -> int

Sourceval equal : t -> t -> bool

Sourceval hash : t -> int

Sourceval transpose : t -> t

Transposes a pair.

Sourceval ith : int -> t -> Atom.t

i-th element of a tuple.

Sourceval is_in_join : t -> t -> t -> bool

is_in_join tuple t1 t2 says whether tuple is the concatenation of t1 (minus the last column) and t2 (minus the ifrst column).

Sourceval join : t -> t -> t

Joins two tuples (getting rid of the last and first columns (resp.))

Sourceval split : t -> int -> t * t

split t lg splits a tuple into two, the first being of length lg.

Sourceval all_different : t -> bool

all_different t tells whether all atoms in a tuple are different.

Sourceval rename : (Atom.t, Atom.t) Containers.List.Assoc.t -> t -> t

Sourceval to_1tuples : t -> t list

to_1tuples t splits a tuple into as many 1-tuples at its length.

Sourceval to_ntuples : int -> t -> t list

to_ntuples n t splits a tuple into n-tuples (length must be a multiple of n).

Sourceval to_list : t -> Atom.t list

to_list t produces a list of atoms.

include Intf.Print.S with type t := t

Sourceval pp : t Fmtc.t

Sourceval to_string : t -> string

Sourcemodule Set : CCSet.S with type elt = t