Michael Norrish
Michael Norrish
I think it's arguable either way. I'd expect the big multiplicative blobs to get normalised so that they turn into things like the example that works.
Yes! Perhaps the magic attribute for this situation should be `deferred` rather than `nested`.
Happy to see a PR along these lines!
I have started to convert the first chapter of the description manual to markdown, from which I can then generate PDFs and HTML (see the generated `system.html` and `system.pdf`). Both...
To be honest, I think this will likely produce much less robust proofs that also become textually larger and grosser. In particular, if you store the details of where to...
If I understand correctly, you would thus be replacing `simp[..]` invocations with something like ``` simp_tac pure_ss [th1, th2, .. , thn, ASSUME “assumption1“, ASSUME “assumption2”, ... ASSUME “assumptions”, SF...
I think someone should be profiling some of the relevant code to see where the slowness is coming from.
If the list of used theorems is small, I can see this being useful, but we would need to profile invocations to see how many get used per invocation to...
Thanks for the report!
I doubt that's the issue; that entry-point is to support users removing things from theorem-sets. There's no way to access that functionality from the user-side of things with `defncong` (perhaps...