Michael Norrish

Actually, `.sig` files can be embedded into HTML files easily enough, as done [here](https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/src-sml/htmlsigs/bagTheory.html). I much prefer that to [this example of the other HTML style](https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/theorygraph/binary_ieeeTheory.html).

No - but happy to be prodded.

Both, thanks.

Actually, casts are unary, so perhaps we could have this as a suffix, so that ``` w1 ₃₂→₁₆ ``` would be the 16 bit value corresponding to `w1`. Alternatively, and...

You actually need to know both source and destination sizes, so in some sense it's a ternary operation. Moreover, the source and dest numbers have to be literals; they're not...

You could define a type `'a finiteUnfolder`, that was a subset of the type ``` 'a -> (char # 'a) option ``` such that `LFINITE (LUNFOLD f s)` held for...

The CakeML semantics could be made explicitly deterministic, without relying on weird properties of the HOL model, by having it use just one canonical NaN at the top level of...

What is the route to reproduction from a clean checkout of `master` please?

Thanks for the description of the failure. Given the dependency, there should be a link to `semantics/proofs` in the `INCLUDES` information for the `compiler/parsing` directory. If any of the script...

If there were a clear specification for what parsingComputeLib is supposed to do, your option 4 might be possible. At a guess, I suppose it's supposed to provide `CBV_CONV`-ability for...