Module Meta.Object

External meta-objects.

type t =
  1. | Context of {
    1. location : Syncom.Location.t;
    2. context : Synext__.Synext_definition.CLF.Context.t;
    }
    (*

    Context { context; _ } is the context meta-object [context].

    *)
  2. | Contextual_term of {
    1. location : Syncom.Location.t;
    2. context : Synext__.Synext_definition.CLF.Context.t;
    3. term : Synext__.Synext_definition.CLF.Term.t;
    }
    (*

    Contextual_term { context; term; _ } is the contextual term [context |- term].

    *)
  3. | Plain_substitution of {
    1. location : Syncom.Location.t;
    2. domain : Synext__.Synext_definition.CLF.Context.t;
    3. range : Synext__.Synext_definition.CLF.Substitution.t;
    }
    (*

    Plain_substitution { domain; range; _ } is the plain substitution $[domain |- range].

    *)
  4. | Renaming_substitution of {
    1. location : Syncom.Location.t;
    2. domain : Synext__.Synext_definition.CLF.Context.t;
    3. range : Synext__.Synext_definition.CLF.Substitution.t;
    }
    (*

    Renaming_substitution { domain; range; _ } is the renaming substitution $[domain |-# range].

    *)