Module Meta.Pattern

External meta-object patterns.

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

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

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

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

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

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

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

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

    *)