Re: [Hol-info] A question about specialization in HOL4

Hi Ada, > But I can't specialize the variaty l in CX_IN with "CAN l". Why can't you specialise it? What methods have you tried? I would have expected that SPEC or ISPEC do work. A common problem are mismatched types. Your definitions look polymorphic to me in the type of list elements. If on

[Hol-info] A question about specialization in HOL4

Hi,guys I am working with HOL4. This is the subgoal > val it = CX (INSERT h (CAN l)) p q = CX (h::l) p q 0. !p q n. (LENGTH p = LENGTH q) ==> (CX (CAN l) p q = CX l p q) 1. LENGTH p = LENGTH q : p