package lascar

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

for outputs and local variables

type name = string

The type of variable names

type value = Value.t

The type for variable values

type t = (name * value) list

The type of valuation. Basic, public implementation here

val compare : t -> t -> int
val to_string : t -> string
exception Invalid_valuation of t
val check : name list -> t -> unit

check names vs checks whether vs is a "complete" valuation wrt. to names. i.e. whether each variable listed in names has a valuation in vs and each variable listed in vs occurs in names. Raises Invalid_valuation in case of failure.

val empty : t
exception Duplicate of name
val add : name -> value -> t -> t
val remove : name -> t -> t
val mem : name -> t -> bool
val assoc : name -> t -> value
val string_of_value : value -> string