Module LF.Typ

External LF types.

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

    Constant { identifier = "c"; _ } is the type-level constant with qualified identifier "c".

    *)
  2. | Application of {
    1. location : Syncom.Location.t;
    2. applicand : t;
    3. arguments : Term.t Support.List1.t;
    }
    (*

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

    If applicand = Typ.Constant _ with resolved operator description operator, then List1.length arguments = Operator.arity operator.

    *)
  3. | Arrow of {
    1. location : Syncom.Location.t;
    2. domain : t;
    3. range : t;
    4. orientation : [ `Forward | `Backward ];
    }
    (*
    • Arrow { domain; range; orientation = `Forward; _ } is the type domain -> range.
    • Arrow { range; domain; orientation = `Backward; _ } is the type range <- domain.
    *)
  4. | Pi of {
    1. location : Syncom.Location.t;
    2. parameter_identifier : Syncom.Identifier.t Support.Option.t;
    3. parameter_type : 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 type { x : t } body. The variable "x" ranges over LF terms.

    *)