Module `Meta.Typ`

External meta-types.

type t =

| Context_schema of {
1. location : Syncom.Location.t;
2. schema : Syncom.Qualified_identifier.t;
}
(*
Context_schema_constant { schema; _ } is the context schema schema.
*)
| Contextual_typ of {
1. location : Syncom.Location.t;
2. context : Synext__.Synext_definition.CLF.Context.t;
3. typ : Synext__.Synext_definition.CLF.Typ.t;
}
(*
Contextual_typ { context; typ; _ } is the contextual type (context |- typ).
*)
| Parameter_typ of {
1. location : Syncom.Location.t;
2. context : Synext__.Synext_definition.CLF.Context.t;
3. typ : Synext__.Synext_definition.CLF.Typ.t;
}
(*
Parameter_typ { context; typ; _ } is the parameter type #(context |- typ).
*)
| Plain_substitution_typ of {
1. location : Syncom.Location.t;
2. domain : Synext__.Synext_definition.CLF.Context.t;
3. range : Synext__.Synext_definition.CLF.Context.t;
}
(*
Plain_substitution_typ { domain; range; _ } is the type for the plain substitution $(domain |- range).
*)
| Renaming_substitution_typ of {
1. location : Syncom.Location.t;
2. domain : Synext__.Synext_definition.CLF.Context.t;
3. range : Synext__.Synext_definition.CLF.Context.t;
}
(*
Renaming_substitution_typ { domain; range; _ } is the type for the renaming substitution $(domain |-# range).
*)