Module Syncom.Depend

Dependency annotations to parameters to dependent type functions.

In dependent function types Πx:A.B, either:

  1. B depends on x
  2. B may or may not depend on x
  3. B does not depend on x (which we usually denote as A → B)

This data type was first introduced in the Twelf system.

type t = private
  1. | Yes
    (*

    The dependent type depends on the parameter.

    In the case of dependent function types, this means that it cannot be an arrow.

    *)
  2. | Maybe
    (*

    The dependent type may or may not depend on the parameter, we just don't know at this point.

    In the case of dependent function types, this means that it can be either an arrow or a Pi-type.

    *)
  3. | No
    (*

    The dependent type does not depend on the parameter.

    In the case of dependent function types, this means that it is actually an arrow.

    *)

The type of annotation for parameters to dependent kinds or types.

In dependent function types Πx:A.B, the depend annotation refers to the relation between x and B.

Constructors

val yes : t

yes is Yes.

val maybe : t

maybe is Maybe.

val no : t

no is No.

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 (=).