Module LF.Kind

External LF kinds.

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

    Typ { _ } is the kind of simple types type.

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

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

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

    Pi { parameter_identifier = Option.Some "x"; parameter_type = Option.Some t; body; _ } is the dependent product kind { x : t } body. The variable "x" ranges over LF terms.

    *)