Konrad Slind

I use HO_MATCH_MP_TAC for such things. --Konrad. On Mon, Aug 31, 2015 at 8:11 PM, Ramana Kumar [email protected] wrote: > I want to be able to use recInduct for functions...

Not sure the congruence rule is quite right. You have m1 = m2 but then the next clause (!xxxx. xxxx = valueOf m1 ==> fm1 xxxx = fm2 xxxx) takes...

Thanks for the simple example. Looks like a revisit to the congruence-rule instantiation code in the TC extractor. On Mon, Jul 4, 2022 at 8:57 PM Michael Norrish ***@***.***> wrote:...

Historical reasons, mainly. Do you have an application needing a huge number of substitutions? Konrad. On Fri, Apr 8, 2016 at 9:46 PM, Jack Gallagher [email protected] wrote: > Currently, functions...

fmap |++ [(k1,v1); ...; (kn,vn)], which I have used in the past, seems not too far away from these proposals. On Fri, Nov 23, 2018 at 5:00 AM Michael Norrish...

This is a general problem. If existing constants are going to be renamed/overloaded, then perhaps the search facilities should look at the overloading maps in order to get all the...

I agree with Thibault. Some additional ..._ERR exceptions could be perhaps be declared for more demanding situations, but HOL_ERR works OK the majority of the time. On Mon, Dec 3,...

I think it's a good idea. It may also be worth understanding where the blow-up occurs. For example, the pairing operator has a type 'a->'b->'a#'b that duplicates. Konrad. On Fri,...

I am only peripherally on this discussion. Think it is generally a good idea. Since a lot of the things to be shared are trees, I was intrigued by the...

Agreed. I was never able to argue Bruno out of the ref. --Konrad. On Fri, Nov 30, 2018 at 8:42 PM Michael Norrish wrote: > The references hidden inside compsets...