sortLeq

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

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

According to whether the types passed to sortLeq as arguments are metarepresented sorts or kinds, we can distinguish the following cases:

• Assume first that both types given as arguments are two sorts $s$ and $s'$. Let $S$ be the set of sorts in $\mathcal{R}$ and let $\leq_{\mathcal{R}}$ be its subsort relation. When $s, s'\in S$, sortLeq returns true if $s\leq_{\mathcal{R}} s'$ and false otherwise. For example,

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

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

• If both types given as arguments are kinds in $\mathcal{R}$, then sortLeq returns false when both kinds are different and true when they are equal. For example,

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

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

• If one type is one sort in $\mathcal{R}$ and the other one is a kind in $\mathcal{R}$, then sortLeq checks whether the given sort belongs to the given kind or not. For example,

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

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