sameKind

The operation sameKind takes as arguments the metarepresentation of a module $\mathcal{R}$ and the metarepresentations of two types, that is, either sorts or kinds.

  op sameKind : Module Type Type ~> Bool [special (...)] .

Let $S$ be the set of sorts in $\mathcal{R}$ and let $\leq_{\mathcal{R}}$ be its subsort relation. When the two types passed as arguments to sameKind are sorts $s, s'\in S$, the operation sameKind returns true if $s$ and $s'$ belong to the same connected component in the subsort ordering $\leq_{\mathcal{R}}$, that is, if they belong to the same kind, and false otherwise. When the two arguments are kinds in $\mathcal{R}$, sameKind returns true when they are indeed the same, and false otherwise. Finally, when one argument is one sort and the other is a kind, this operation ckecks whether the sort belongs to the kind.

For example, we have the following reductions about sorts and kinds in the module NUMBERS.

  Maude> reduce in META-LEVEL :
           sameKind(upModule('NUMBERS, false), 'Zero, 'NzNat) .
  result Bool: true

  Maude> reduce in META-LEVEL :
           sameKind(upModule('NUMBERS, false), 'Zero, 'Nat3) .
  result Bool: false

  Maude> reduce in META-LEVEL :
          sameKind(upModule('NUMBERS, false), '`[Zero`], '`[NzNat`]) .
  result Bool: true

  Maude> reduce in META-LEVEL :
           sameKind(upModule('NUMBERS, false), '`[Zero`], 'NzNat) .
  result Bool: true