Hi Lu,
That message comes from the parser, when
unconstrained type variables remain after
type inference. So it seems that you are making
an invocation
match_term `` ...`` `` ... ``;
where one or both of the terms involved are
being parsed. If you don't want to see any
messages you can do
Globals.notify_on_tyvar_guess := false;
If you want finer control, you'll have to make
the invocation of the parser as part of a
function call, e.g.
Lib.with_flag
(Globals.notify_on_tyvar_guess,false)
(fn () => match_term ``foo x`` ``FACT 3``)
();
(This isn't the most transparent example, alas.)
Konrad.
On May 27, 2009, at 6:05 PM, Lu Zhao wrote:
> Hi,
>
> When I use match_term with some types unspecified, HOL always
> generates
> a message similar to the following:
>
> <<HOL message: inventing new type variable names: 'a, 'b>>
>
> Is there a way to depress the message so that I don't have to see a
> long
> list of messages. Specifying the types is not a good option since the
> matched terms have multiple types at the same sub-term position.
>
> Thanks a lot.
> Lu
>
> ----------------------------------------------------------------------
> --------
> Register Now for Creativity and Technology (CaT), June 3rd, NYC. CaT
> is a gathering of tech-side developers & brand creativity
> professionals. Meet
> the minds behind Google Creative Lab, Visual Complexity, Processing, &
> iPhoneDevCamp as they present alongside digital heavyweights like
> Barbarian
> Group, R/GA, & Big Spaceship. http://p.sf.net/sfu/creativitycat-com
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Register Now for Creativity and Technology (CaT), June 3rd, NYC. CaT
is a gathering of tech-side developers & brand creativity professionals. Meet
the minds behind Google Creative Lab, Visual Complexity, Processing, &
iPhoneDevCamp as they present alongside digital heavyweights like Barbarian
Group, R/GA, & Big Spaceship. http://p.sf.net/sfu/creativitycat-com
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
