Flesh out the reference section for spec expressions

[tjhance]

Flesh out some reference documentation, with a focus on clarifying the semantics of spec code.

• Add a types page that explains the mathematical interpretation of most builtin types. (entirely written by me)
• Flesh out the spec expression pages.
  • These now have a mostly full "grammar" defined, except for the expressions that we don't have pages for yet (closures, ->, matches, is). There's a postprocessor script to make the grammars look pretty and hyperlink them together (written by claude).
  • Most of the expression pages are now fleshed out with dedicates 'syntax', 'typing', and 'semantics' subheadings.
  • Claude helped with some of these (it was really bad at first, but did OK after I got the basic structure in place. (Though I was particularly impressed by its decision on how to handle triggers: ""Triggers" became a fourth ### section rather than a subsection of Semantics — it's substantial enough and distinct enough (it's about proof-system mechanics, not just the mathematical meaning) to merit its own heading." This is entirely correct but fairly subtle and not something I had expected it to pick up))

The idea behind the notation is V@ for Verus concepts (like spec_expr) and R@ for standard Rust concepts.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.