On 13/03/10 03:14, [email protected] wrote: > ------------------------------------------------------------ > Even I checked the type of "IMAGE (\k. {s | FST (f k s) = (x l) k}) > (count (SUC n))", it shows that it is exact the type of "c" in thereom > EVENTS_COUNTABLE_INTER. More else, I failed to solve this problem by > using "Q.ABBREV_TAC" to make this "IMAGE (\k. {s | FST (f k s) = (x l) > k}) (count (SUC n))" simple. > ------------------------------------------------------------ > - type_of ``IMAGE (\k. {s | FST (f k s) = (x l) k}) (count (SUC n))``; > <<HOL message: more than one resolution of overloading was possible>> > <<HOL message: inventing new type variable names: 'a, 'b, 'c, 'd>> >> val it = ``:('a -> bool) -> bool`` : hol_type > ------------------------------------------------------------
I'd be suspicious of this message. Why are there multiple overloading resolutions possible in the term you give? If you do term_grammar(), what do you see in the overloading section for the strings "count", "SUC", "IMAGE" and "FST"? In particular, does each map to just one constant, and does each map to the constant you expect. Also, are you using the examples/miller probability theory, or the one under src? Michael ------------------------------------------------------------------------------ Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and fine-tune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intel-sw-dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
