[minor] Named asserts, various fixes

[tnelson]

Sterling Update

Added two features:

• A "Help" button in the lower bar that gives instructions on the view mode currently selected. E.g., the evaluator, timing, zooming on trackpad using two fingers rather than pinch and drag, etc.
• The default visualizer will now show the most-specific sig name that the atom inhabits in this instance (or state, if the instance is temporal). At the moment, this annotation cannot be themed, but this avoids the need for a dynamic atom-renaming strategy like Alloy 6 uses.

Named assertions

Assertions can now be named, similarly to run. E.g.,

someBsat: assert {some B} is sat
emptyBunsat: assert {no B} is unsat 
BsufficientA: assert B is sufficient for A
BnecessaryA: assert B is necessary for A
BconsistentWithA: assert B is consistent with A

Recall that assertions can receive bounds, just like run commands:

someBsat: assert {some B} is sat for 5 A, 4, B
wellformedTraceSat: assert {wellformed} is sat for 10 State for {next is linear}

Fixes and Experimental Features

Predicate typechecking

Previously, predicate type checking could infer an argument of type univ (meaning any type), but report Int. This was caused by the error system selecting the first of a list of options (which, in the case of univ, was a list of all possible sigs). This should no longer happen, as the list of sigs is now compressed by combining child sigs that cover all possibilities in the parent.

Extending Int (Experimental)

Fixed an issue when a sig is declared that extends Int. This is now running and tested, but has not been exercised much yet. Treat the feature as experimental.