lesserSorts

The operation lesserSorts takes as arguments the metarepresentation of a module $\mathcal{R}$ and the metarepresentation of a type, i.e., a sort or a kind.

  op lesserSorts : Module Type ~> SortSet [special (...)] .

Let $S$ be the set of sorts in $\mathcal{R}$. When $s\in S$, lesserSorts returns the metarepresentation of the set of sorts strictly smaller than $s$ in $S$. For example,

  Maude> reduce in META-LEVEL : 
           lesserSorts(upModule('NUMBERS, false), 'Nat) .
  result NeSortSet: 'NzNat ; 'Zero

  Maude> reduce in META-LEVEL : 
           lesserSorts(upModule('NUMBERS, false), 'Zero) .
  result EmptyTypeSet: (none).EmptyTypeSet

  Maude> reduce in META-LEVEL : 
           lesserSorts(upModule('NUMBERS, false), 'NatSeq) .
  result NeSortSet: 'Nat ; 'NzNat ; 'Zero

When the second argument of lesserSorts metarepresents a kind in $\mathcal{R}$, this operation returns the metarepresentation of the set of all sorts in such kind. For example,

  Maude> reduce in META-LEVEL : 
           lesserSorts(upModule('NUMBERS, false), '`[NatSeq`]) .
  result NeSortSet: 'Nat ; 'NatSeq ; 'NatSet ; 'NzNat ; 'Zero

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