module z/anno/ZTerm
imports
  z/ZTerm
exports
  sorts Pred ZExpr
  context-free syntax
    "∀" ZExpr "⦁" ZTerm    -> ZTerm {cons("ZAllTerm")}
    "∃↘1↖" ZExpr "⦁" ZTerm -> ZTerm {cons("ZExiOneTerm")}

    "μ" ZExpr "⦁" ZTerm     -> ZTerm {cons("ZMuExpr")}
    "{" ZExpr "⦁" ZTerm "}" -> ZTerm {cons("ZSetComp")}
    "[" ZName ":" ZExpr "]" -> ZTerm {cons("ZVarConst")}
    "[" ZExpr "|" Pred "]"  -> ZTerm {cons("ZSchConst")}
  context-free priorities
    ZTerm "⨟" ZTerm -> ZTerm >
    "μ" ZExpr "⦁" ZTerm -> ZTerm >
    { left: ZTerm "∈" ZTerm -> ZTerm
    } >
    "¬" ZTerm -> ZTerm >
    ZTerm "∧" ZTerm -> ZTerm >
    { left: "∀" ZExpr "⦁" ZTerm -> ZTerm
	    "∃↘1↖" ZExpr "⦁" ZTerm -> ZTerm
    }
