Module Comp.Kind

External computation-level kinds.

type t =
  1. | Ctype of {
    1. location : Syncom.Location.t;
    }
    (*

    Ctype { _ } is the kind of computation-level types ctype.

    *)
  2. | Arrow of {
    1. location : Syncom.Location.t;
    2. domain : Synext__.Synext_definition.Meta.Typ.t;
    3. range : t;
    }
    (*

    Arrow { domain; range; _ } is the computation-level kind domain -> range.

    *)
  3. | Pi of {
    1. location : Syncom.Location.t;
    2. parameter_identifier : Syncom.Identifier.t Support.Option.t;
    3. plicity : Syncom.Plicity.t;
    4. parameter_type : Synext__.Synext_definition.Meta.Typ.t;
    5. body : t;
    }
    (*

    Pi { parameter_identifier = Option.Some "x"; parameter_type = t; explicit; body; _ } is the explicit dependent product kind { x : t } body if plicity = Plicity.Explicit, and the implicit dependent product kind (x : t) body if plicity = Plicity.Implicit. The variable "x" ranges over meta-level objects.

    *)