Add syntactic access to underlying sets

[GuiltyDolphin]

We should have a means of accessing the underlying sets (and their operations) of semirings.

Currently, for example, if you have a semiring whose underlying set is the natural numbers, but whose additive identity is not the 0 of the natural numbers, then there is no way to access this element.

This would be based on the standard operations of the set, and thus we could have more operations than just those permitted by a semiring.

List of operations:

• .n - underlying element of the semiring set, e.g., .0 is the 0 of the set, not of the semiring
• .+ - underlying addition
• .* - underlying multiplication
• .min - underlying minimum (i.e., meet) (e.g., for natural-number semirings this would be based on a usual ordering)
• etc.

Then the non-dotted versions will always refer to the semirings in question, not their underlying sets.

@dorchard we discussed this in Slack. I'm just making an issue here so that we don't lose track of this idea.

[GuiltyDolphin]

Marked as 'On Hold' pending completion of merges of current large pull requests, to avoid additional conflicts.

[dorchard]

Whilst trying to square away some other things, I'm doing a partial implementation of this where .n is marked as definitely a natural number inside the type checker.

[dorchard]

Also in progress on type-nonix branch on this, ".<=" means natural number less than equal but "<=" means semiring preorder (and similarly for ".>=" and ">=" (invert semiring preorder)).

[dorchard]

This feature can now go ahead and is partially implemented already on dev-minor: .n means treat n really as a natural number and .<= and .>= mean use the natural number ordering