module alloy/Modules
imports
  alloy/Names

exports
  sorts Module Name0 Number0

  context-free syntax
  "module" Name ("["  Name0  ("," Number0)*    "]" )? -> Module {cons("AlloyModule")}

  "exactly" Name -> Name0 {cons("AExactName")}
  Name -> Name0

  "exactly" Number -> Number0 {cons("AExactNumber")}
  Number -> Number0