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 : Mode.Modality.Const.t

The identity modality.

val is_id : Mode.Modality.Const.t -> bool

Test if the given modality is the identity modality.

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

Apply a modality on mode.

val concat : 
  then_:Mode.Modality.Const.t ->
  Mode.Modality.Const.t ->
  Mode.Modality.Const.t

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

val set : 
  'a Mode.Modality.Axis.t ->
  'a ->
  Mode.Modality.Const.t ->
  Mode.Modality.Const.t

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

val proj : 'a Mode.Modality.Axis.t -> Mode.Modality.Const.t -> 'a

proj ax t projects out the axis ax of t.

val diff : 
  Mode.Modality.Const.t ->
  Mode.Modality.Const.t ->
  Mode.Modality.atom list

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

val equate : 
  Mode.Modality.Const.t ->
  Mode.Modality.Const.t ->
  (unit, Mode.Modality.equate_error) Stdlib.Result.t

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

val print : Stdlib.Format.formatter -> Mode.Modality.Const.t -> unit

Printing for debugging.

Module Modality.Const