Michael Norrish comments

Results 238 comments of


                                            Michael Norrish

Build failure in 32-bit mode: Structure (Word64) has not been declared

Ha! Thanks for the report; I hadn't appreciated this might be a problem. I will have to detect the build-time information about the build size, and then make the code...

Consider using OpenTheory for persistent theories

I don't think so. I assume the original suggestion was to store open-theory proofs as permanent records of theorems. In contrast, the `otknl` approach *generates* open-theory proofs as build products.

Name in namedCases should not be renamed if it already exists

This is an interesting one. I eventually want to subsume this awful soup (`namedCases`, `pairCases` urge) into a more potent `Cases_on` tactic, but I think if the user has gone...

Rename should not rewrite assumptions multiple times

Thanks for the issue. I agree that this would be nice. Note that it is reasonable to have `rename` list elements targeting separate parts of the same assumption, but this...

Speed up net filtering by names in the simplifier

It's slow but called very infrequently; this doesn't feel like a high priority.

Remove the use of `free_vars` in HO_PART_MATCH

I'd be happy to receive a PR along these lines.

Fuse strlit and implode in mlstringTheory

You could keep an overload in place to simplify your first task.

Implement net mapping relations to congprocs/weakenprocs for performance

Agreed that this would be a great tweak!