Module Modality.Const

type t

A modality that acts on Value axes. Conceptually it is a record where individual fields can be set or proj.

val id : t

The identity modality.

val is_id : t -> bool

Test if the given modality is the identity modality.

val apply : t -> ('l * 'r) Value.t -> ('l * 'r) Value.t

Apply a modality on mode.

val concat : then_:t -> t -> t

concat ~then t returns the modality that is then_ after t.

val set : 'a Axis.t -> 'a -> t -> t

set a t overwrites an axis of t to be a.

val proj : 'a Axis.t -> t -> 'a

proj ax t projects out the axis ax of t.

val diff : t -> t -> atom list

diff t0 t1 returns a list of atoms in t1 that are different than t0.

val equate : t -> t -> (unit, equate_error) Result.t

equate t0 t1 checks that t0 = t1. Definition: t0 = t1 iff t0 <= t1 and t1 <= t0.

val print : Format.formatter -> t -> unit

Printing for debugging.