Module Comp.Typ

External computation-level types.

type t =
  1. | Inductive_typ_constant of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Qualified_identifier.t;
    }
    (*

    Inductive_typ_constant { identifier = "c"; } is the computation-level inductive type constant "c".

    *)
  2. | Stratified_typ_constant of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Qualified_identifier.t;
    }
    (*

    Stratified_typ_constant { identifier = "c"; } is the computation-level stratified type constant "c".

    *)
  3. | Coinductive_typ_constant of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Qualified_identifier.t;
    }
    (*

    Coinductive_typ_constant { identifier = "c"; } is the computation-level coinductive type constant "c".

    *)
  4. | Abbreviation_typ_constant of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Qualified_identifier.t;
    }
    (*

    Abbreviation_typ_constant { identifier = "c"; } is the computation-level abbreviated type constant "c".

    *)
  5. | 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 type { x : t } body if plicity = Plicity.Explicit, and the implicit dependent product type (x : t) body if plicity = Plicity.Implicit. The variable "x" ranges over computation-level terms.

    *)
  6. | Arrow of {
    1. location : Syncom.Location.t;
    2. domain : t;
    3. range : t;
    4. orientation : [ `Forward | `Backward ];
    }
    (*

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

    *)
  7. | Cross of {
    1. location : Syncom.Location.t;
    2. types : t Support.List2.t;
    }
    (*

    Cross { typs = [t1; t2; ...; tn]; _ } is the type of tuple t1 * t2 * ... * tn.

    *)
  8. | Box of {
    1. location : Syncom.Location.t;
    2. meta_type : Synext__.Synext_definition.Meta.Typ.t;
    }
    (*

    Box { typ = u; _ } is a boxed meta-type [u].

    *)
  9. | Application of {
    1. location : Syncom.Location.t;
    2. applicand : t;
    3. arguments : Synext__.Synext_definition.Meta.Object.t Support.List1.t;
    }
    (*

    Application { applicand; arguments; _ } is the application of applicand with arguments.

    If applicand = Typ.Inductive_typ_constant | Typ.Stratified_typ_constant _ | Typ.Coinductive_typ_constant _ | Typ.Abbreviation_typ_constant _ with resolved operator description operator, then List1.nth arguments = Operator.arity operator.

    *)