Module Syncom.Plicity

Annotations for implicit or explicit parameters.

type t = private
  1. | Implicit
    (*

    The annotation for implicit parameters.

    *)
  2. | Explicit
    (*

    The annotation for explicit parameters.

    *)

The type of annotation for implicit or explicit parameters.

A parameter is implicit if

  • it was specified by the user as (g : ctx) in the external syntax, or
  • it was generated during reconstruction.

A parameter is explicit if it was specified by the user as {g : ctx} in the external syntax.

Constructors

val implicit : t

implicit is Implicit.

val explicit : t

explicit is Explicit.

Predicates and comparisons

val max : t -> t -> t

max p1 p2 is Explicit if at least one of p1 and p2 is Explicit. Otherwise, Implicit is returned.

val is_explicit : t -> bool

is_explicit p is true if and only if p is Explicit.

val is_implicit : t -> bool

is_implicit p is true if and only if p is Implicit.

Instances

include Support.Eq.EQ with type t := t
val equal : t -> t -> bool

equal a b is true if and only if a and b are equal. This should satisfy the following properties:

  • Reflexivity: equal a a = true
  • Symmetry: equal a b is equivalent to equal b a
  • Transitivity: if equal a b = true and equal b c = true, then equal a c = true
val (=) : t -> t -> bool

Operator alias of equal.

val (<>) : t -> t -> bool

Negation of operator (=).