myreen

I doubt proof replay on load would be tolerable. Anyway, how large would these proofs be? My impression is that real proof developments produce enormous OpenTheory proofs. On 7 August...

> Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles...

This kind of description could go somewhere towards the end of the existing how-to.md.

Closing because this PR has been continued as #1022.

For `map`, the `specialise` function should actually generate: ``` specialise `map` `lam f xs -> ... f ... map f ys ...` = SOME `lam f -> letrec map =...

I would prefer there to be a switch which determines whether `astPP` is to produce SML or CakeML.

I'm often annoyed by the names of the generated side conditions. The reason for the odd names is that the translator tries to not redefine already defined functions. Would it...

@mn200 are you suggesting by "if it's to be defined at all" that `read_bytearray` should be an overloading as follows? read_bytearray a c gb = OPT_MMAP gb (GENLIST (λi. a...

This conversation reminds me of `byteTheory` as proposed in #521.

The `delete_const` at the end there might be a bit too destructive since some people give HOL the entire script file (including the `export_theory` line) when starting their session. My...