Summary
- merged
- Tuned text
- clarified signature: avoid confusion due to redundant standard_path, which is already used here (but not elsewhere);
- clarified signature: avoid case class with redefined equality;
- discontinued somewhat pointless dependency: avoid illusion of extra accuracy (see also 09fb749d1a1e and 0f750a6dc754);
- tuned;
- clarified signature;
- unused;
- clarified signature;
- tuned whitespace;
- tuned;
- clarified signature;
- tuned signature;
- tuned output;
- prefer SML here
- Typo.