Module AltErgoLib.Literal

This module contains a definition of a "combined" literal type that can contain both syntaxic literals (expressions) and semantic literals (that contain semantic values, see also the Xliteral module).

type 'a view =
  1. | LTerm of Expr.t
  2. | LSem of 'a
    (*

    View over literals, parameterized by the type of semantic literals. Used for both pattern-matching and creation of literals (through the make and view functions).

    *)
val pp_view : 'a Fmt.t -> 'a view Fmt.t

Pretty-printer for views.

val hash_view : ('a -> int) -> 'a view -> int

Hash function for views.

val equal_view : ('a -> 'a -> bool) -> 'a view -> 'a view -> bool

Equality function for views.

val compare_view : ('a -> 'a -> int) -> 'a view -> 'a view -> int

Comparison function for views.

module type S = sig ... end
module Make (Sem : Xliteral.S) : S with type elt = Sem.t