Module Settings

Global settings.

val disable_pasting_check : bool Stdlib.ref

Whether checking for pasting types is disabled.

type mode = [
  1. | `Plain
  2. | `Category
  3. | `Monoidal
  4. | `Symmetric_monoidal
  5. | `Symmetric_monoidal_closed
  6. | `Linear_closed
  7. | `Cartesian
  8. | `Cartesian_closed
  9. | `Compact_closed
]

Mode for checking pasting schemes.

val mode : mode Stdlib.ref
val has_hom : unit -> bool
val has_prod : unit -> bool
val has_one : unit -> bool
val elements : bool Stdlib.ref
val set_elements : bool -> unit
val has_elements : unit -> bool

Whether types have elements, ie we consider x : a as implicitly meaning x : 1 → a.

val has_op : unit -> bool
val mode_callback : (mode -> unit) Stdlib.ref

Callback when the mode is changed.

val on_mode : (mode -> unit) -> unit
val dim_callback : (int -> unit) Stdlib.ref

Callback when the dimension is changed.

val dimension : int Stdlib.ref

Maximal depth for pasting schemes.

val on_dim : (int -> unit) -> unit
val set_dim : int -> unit
val orientation : [ `Directed | `Reversible ] Stdlib.ref

Whether all maps are reversible starting from dimension 1.

val orientation_callback : ([ `Directed | `Reversible ] -> unit) Stdlib.ref
val on_orientation : ([ `Directed | `Reversible ] -> unit) -> unit
val set_orientation : [ `Directed | `Reversible ] -> unit
val ordered : bool Stdlib.ref

When set to true, we use the order on cells in order to determine whether we are pasting.

val set_ordered : bool -> unit
val parse : string -> unit
val save : unit -> unit
val restore : unit -> unit