module z/ext/ISOMetalanguage
imports
  z/ZTerm
exports
  context-free syntax
    "〚" ZTerm "〛"  -> ZTerm {cons("ZSemantics")}

    "∅"             -> ZTerm {cons("ZEmptySetExpr")}
    ZTerm "∖" ZTerm -> ZTerm {cons("ZSetMinusExpr")}
    ZTerm "∪" ZTerm -> ZTerm {cons("ZSetUnionExpr")}
    ZTerm "∩" ZTerm -> ZTerm {cons("ZSetIntersectionExpr")}
    ZTerm "⊕" ZTerm -> ZTerm {cons("ZOPlusExpr")}
    ZTerm "↦" ZTerm -> ZTerm {cons("ZMapstoExpr")}
 
   context-free priorities
     ZTerm ZTerm -> ZTerm >
     ZTerm "∪" ZTerm -> ZTerm >
     ZTerm "↦" ZTerm -> ZTerm >
     {
       left: {ZTerm "×"}+ -> ZTerm
             ZTerm -> {ZTerm "×"}+
     } 