Michael Norrish
Michael Norrish
I’ll give it a go.
I've made what I think is the appropriate update to the definition of `float_mul_add`. Is there an analogous update that should be made to `float_mul_sub`? I've included your test-case from...
Absolutely. Of course, if the "alternative" were pursued, not all superscripts would have to be made non-aggregating, and the numeral superscripts would have to stay as they are. We would...
On 6/09/11 5:08 PM, xrchz wrote: > When? By the simplifier? Yeah; in srw_ss() with an appropriate conversion.
Better yet (perhaps?): detect if FS is case-insensitive, record this fact, and then change operations like `load` to normalise filenames before using then.
The flagging of theorems, whether white-listing (with associated categories?) or marking as interesting could obviously be done with theorem attributes.
Yeah, I think you're right.
Don't know how keen I am on this when existing monad syntax would also work. For example ```` [ x + 1 | x
I think the syntax here should use a string argument, and that the string should then be encoded into the “using assumption”. (One might imagine changing the type of tactics...
As you say, `ho_match_mp_tac` doesn't do all that `Induct_on` does. And in fact, I want `Induct_on` to do still more. For example, when working with `FINITE_INDUCT`, have it cope with...