Re: [isabelle] string -> const



On Mon, 13 Feb 2006, Sean McLaughlin wrote:

> Is there a way to go from a string to a const without incurring error 
> messages? EG.  Right now I have:
> 
> fun type_of_const c = type_of (read c) handle _ => type_of (read ("op " ^ c))

Just note that handling *any* exception with a "_" pattern is a bad idea. 
This would also cover Interrupt raised by user interaction, which is not 
what you want here.  The above can be made to work using 
Output.transform_error, but it is easier to avoid user-level functions 
like "read" in the first place.

Just use Sign.const_type, maybe after Sign.intern_const if name space 
lookup should be included as well.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.