Konrad Slind

Looks like you are describing two things. I don't quite seeing the "using" infix helping with alternate inductions, since if you already have the induction theorem to hand, then ho_match_mp_tac...

As you mentioned, I don't see how stashing things on the assumptions will help apply polymorphic ind. thms. On Mon, Nov 19, 2018 at 7:03 PM Michael Norrish wrote: >...

Ah I see! On Wed, Nov 21, 2018 at 7:38 PM Michael Norrish wrote: > You stash the name of the theorem, encoded as variable (using, K T name >...

The latter, of course, is inaccessible, but just thought I'd mention it.

Well, David Russinoff did this kind of thing for AMD, and he's now at ARM, presumably doing the same thing. So maybe it's just a matter of finding and formalizing...

Possibly naive question. Why not have a general operation width(w,n) which maps word w to its corresponding n-width version? Being binary, the "width" operation could even be an infix, although...

Right. I was operating under the assumption that w would have a type from which its size could be calculated. (I did this in a language we worked on at...

Related work: https://hal.archives-ouvertes.fr/hal-02149909/document On Mon, Nov 16, 2020 at 8:07 AM myreen wrote: > Deflate is a lossless data > compression file format that zip > and gzip > are...

How is this different/better than HO_MATCH_MP_TAC relationTheory.RTC_ALT_RIGHT_INDUCT? Is there some kind of normalization/search for an expression in the goal with RTC as its operator? On Wed, Nov 16, 2022 at...

multiDefine will support lists of definitions, so the proposed syntax could be more liberal. On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish ***@***.***> wrote: > One possibility >...